Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  neibastop2 Structured version   Visualization version   GIF version

Theorem neibastop2 32654
Description: In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
neibastop1.1 (𝜑𝑋𝑉)
neibastop1.2 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
neibastop1.3 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
neibastop1.4 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
neibastop1.5 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
neibastop1.6 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
Assertion
Ref Expression
neibastop2 ((𝜑𝑃𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
Distinct variable groups:   𝑣,𝑡,𝑦,𝑥   𝑣,𝐽   𝑥,𝑦,𝐽   𝑡,𝑜,𝑣,𝑤,𝑥,𝑦,𝑃   𝑜,𝑁,𝑡,𝑣,𝑤,𝑥,𝑦   𝑜,𝐹,𝑡,𝑣,𝑤,𝑥,𝑦   𝜑,𝑜,𝑡,𝑣,𝑤,𝑥,𝑦   𝑜,𝑋,𝑡,𝑣,𝑤,𝑥,𝑦
Allowed substitution hints:   𝐽(𝑤,𝑡,𝑜)   𝑉(𝑥,𝑦,𝑤,𝑣,𝑡,𝑜)

Proof of Theorem neibastop2
Dummy variables 𝑓 𝑛 𝑧 𝑠 𝑢 𝑎 𝑏 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neibastop1.1 . . . . . . . . 9 (𝜑𝑋𝑉)
2 neibastop1.2 . . . . . . . . 9 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
3 neibastop1.3 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
4 neibastop1.4 . . . . . . . . 9 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
51, 2, 3, 4neibastop1 32652 . . . . . . . 8 (𝜑𝐽 ∈ (TopOn‘𝑋))
6 topontop 20912 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
75, 6syl 17 . . . . . . 7 (𝜑𝐽 ∈ Top)
87adantr 472 . . . . . 6 ((𝜑𝑃𝑋) → 𝐽 ∈ Top)
9 eqid 2752 . . . . . . 7 𝐽 = 𝐽
109neii1 21104 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 𝐽)
118, 10sylan 489 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 𝐽)
12 toponuni 20913 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
135, 12syl 17 . . . . . 6 (𝜑𝑋 = 𝐽)
1413ad2antrr 764 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑋 = 𝐽)
1511, 14sseqtr4d 3775 . . . 4 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁𝑋)
16 neii2 21106 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦𝐽 ({𝑃} ⊆ 𝑦𝑦𝑁))
178, 16sylan 489 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦𝐽 ({𝑃} ⊆ 𝑦𝑦𝑁))
18 pweq 4297 . . . . . . . . . . 11 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
1918ineq2d 3949 . . . . . . . . . 10 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
2019neeq1d 2983 . . . . . . . . 9 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
2120raleqbi1dv 3277 . . . . . . . 8 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
2221, 4elrab2 3499 . . . . . . 7 (𝑦𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
23 simprrr 824 . . . . . . . . . . . . 13 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → 𝑦𝑁)
24 sspwb 5058 . . . . . . . . . . . . 13 (𝑦𝑁 ↔ 𝒫 𝑦 ⊆ 𝒫 𝑁)
2523, 24sylib 208 . . . . . . . . . . . 12 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → 𝒫 𝑦 ⊆ 𝒫 𝑁)
26 sslin 3974 . . . . . . . . . . . 12 (𝒫 𝑦 ⊆ 𝒫 𝑁 → ((𝐹𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹𝑃) ∩ 𝒫 𝑁))
2725, 26syl 17 . . . . . . . . . . 11 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → ((𝐹𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹𝑃) ∩ 𝒫 𝑁))
28 simprrl 823 . . . . . . . . . . . . 13 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → {𝑃} ⊆ 𝑦)
29 snssg 4451 . . . . . . . . . . . . . 14 (𝑃𝑋 → (𝑃𝑦 ↔ {𝑃} ⊆ 𝑦))
3029ad3antlr 769 . . . . . . . . . . . . 13 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → (𝑃𝑦 ↔ {𝑃} ⊆ 𝑦))
3128, 30mpbird 247 . . . . . . . . . . . 12 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → 𝑃𝑦)
32 fveq2 6344 . . . . . . . . . . . . . . 15 (𝑥 = 𝑃 → (𝐹𝑥) = (𝐹𝑃))
3332ineq1d 3948 . . . . . . . . . . . . . 14 (𝑥 = 𝑃 → ((𝐹𝑥) ∩ 𝒫 𝑦) = ((𝐹𝑃) ∩ 𝒫 𝑦))
3433neeq1d 2983 . . . . . . . . . . . . 13 (𝑥 = 𝑃 → (((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅))
3534rspcv 3437 . . . . . . . . . . . 12 (𝑃𝑦 → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅))
3631, 35syl 17 . . . . . . . . . . 11 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅))
37 ssn0 4111 . . . . . . . . . . 11 ((((𝐹𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹𝑃) ∩ 𝒫 𝑁) ∧ ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)
3827, 36, 37syl6an 569 . . . . . . . . . 10 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅))
3938expr 644 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (({𝑃} ⊆ 𝑦𝑦𝑁) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
4039com23 86 . . . . . . . 8 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → (({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
4140expimpd 630 . . . . . . 7 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) → (({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
4222, 41syl5bi 232 . . . . . 6 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑦𝐽 → (({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
4342rexlimdv 3160 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (∃𝑦𝐽 ({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅))
4417, 43mpd 15 . . . 4 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)
4515, 44jca 555 . . 3 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅))
4645ex 449 . 2 ((𝜑𝑃𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) → (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
47 n0 4066 . . . 4 (((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁))
48 elin 3931 . . . . . 6 (𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁) ↔ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))
49 simprl 811 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁𝑋)
5013ad2antrr 764 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 = 𝐽)
5149, 50sseqtrd 3774 . . . . . . . 8 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 𝐽)
521ad2antrr 764 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋𝑉)
532ad2antrr 764 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
54 simpll 807 . . . . . . . . . 10 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝜑)
5554, 3sylan 489 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
56 neibastop1.5 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
5754, 56sylan 489 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
58 neibastop1.6 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
5954, 58sylan 489 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
60 simplr 809 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃𝑋)
61 simprrl 823 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ (𝐹𝑃))
62 simprrr 824 . . . . . . . . . 10 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ 𝒫 𝑁)
6362elpwid 4306 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠𝑁)
64 fveq2 6344 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → (𝐹𝑛) = (𝐹𝑥))
6564ineq1d 3948 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → ((𝐹𝑛) ∩ 𝒫 𝑏) = ((𝐹𝑥) ∩ 𝒫 𝑏))
6665cbviunv 4703 . . . . . . . . . . . . . 14 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏) = 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑏)
67 pweq 4297 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧)
6867ineq2d 3949 . . . . . . . . . . . . . . 15 (𝑏 = 𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑏) = ((𝐹𝑥) ∩ 𝒫 𝑧))
6968iuneq2d 4691 . . . . . . . . . . . . . 14 (𝑏 = 𝑧 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑏) = 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
7066, 69syl5eq 2798 . . . . . . . . . . . . 13 (𝑏 = 𝑧 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏) = 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
7170cbviunv 4703 . . . . . . . . . . . 12 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏) = 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)
7271mpteq2i 4885 . . . . . . . . . . 11 (𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
73 rdgeq1 7668 . . . . . . . . . . 11 ((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)) → rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑠}))
7472, 73ax-mp 5 . . . . . . . . . 10 rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑠})
7574reseq1i 5539 . . . . . . . . 9 (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω) = (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑠}) ↾ ω)
76 pweq 4297 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓)
7776ineq2d 3949 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → ((𝐹𝑤) ∩ 𝒫 𝑔) = ((𝐹𝑤) ∩ 𝒫 𝑓))
7877neeq1d 2983 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅))
7978cbvrexv 3303 . . . . . . . . . . 11 (∃𝑔 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅)
80 fveq2 6344 . . . . . . . . . . . . . 14 (𝑤 = 𝑦 → (𝐹𝑤) = (𝐹𝑦))
8180ineq1d 3948 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → ((𝐹𝑤) ∩ 𝒫 𝑓) = ((𝐹𝑦) ∩ 𝒫 𝑓))
8281neeq1d 2983 . . . . . . . . . . . 12 (𝑤 = 𝑦 → (((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
8382rexbidv 3182 . . . . . . . . . . 11 (𝑤 = 𝑦 → (∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
8479, 83syl5bb 272 . . . . . . . . . 10 (𝑤 = 𝑦 → (∃𝑔 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
8584cbvrabv 3331 . . . . . . . . 9 {𝑤𝑋 ∣ ∃𝑔 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅} = {𝑦𝑋 ∣ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅}
8652, 53, 55, 4, 57, 59, 60, 49, 61, 63, 75, 85neibastop2lem 32653 . . . . . . . 8 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
877ad2antrr 764 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐽 ∈ Top)
8860, 50eleqtrd 2833 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 𝐽)
899isneip 21103 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑃 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 𝐽 ∧ ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))))
9087, 88, 89syl2anc 696 . . . . . . . 8 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 𝐽 ∧ ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))))
9151, 86, 90mpbir2and 995 . . . . . . 7 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
9291expr 644 . . . . . 6 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → ((𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9348, 92syl5bi 232 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → (𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9493exlimdv 2002 . . . 4 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → (∃𝑠 𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9547, 94syl5bi 232 . . 3 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → (((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅ → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9695expimpd 630 . 2 ((𝜑𝑃𝑋) → ((𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9746, 96impbid 202 1 ((𝜑𝑃𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1624  wex 1845  wcel 2131  wne 2924  wral 3042  wrex 3043  {crab 3046  Vcvv 3332  cdif 3704  cin 3706  wss 3707  c0 4050  𝒫 cpw 4294  {csn 4313   cuni 4580   ciun 4664  cmpt 4873  ran crn 5259  cres 5260  wf 6037  cfv 6041  ωcom 7222  reccrdg 7666  Topctop 20892  TopOnctopon 20909  neicnei 21095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-reu 3049  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-om 7223  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-top 20893  df-topon 20910  df-nei 21096
This theorem is referenced by:  neibastop3  32655
  Copyright terms: Public domain W3C validator