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 34321
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 34319 . . . . . . . 8 (𝜑𝐽 ∈ (TopOn‘𝑋))
6 topontop 21842 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
75, 6syl 17 . . . . . . 7 (𝜑𝐽 ∈ Top)
87adantr 484 . . . . . 6 ((𝜑𝑃𝑋) → 𝐽 ∈ Top)
9 eqid 2739 . . . . . . 7 𝐽 = 𝐽
109neii1 22035 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 𝐽)
118, 10sylan 583 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 𝐽)
12 toponuni 21843 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
135, 12syl 17 . . . . . 6 (𝜑𝑋 = 𝐽)
1413ad2antrr 726 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑋 = 𝐽)
1511, 14sseqtrrd 3959 . . . 4 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁𝑋)
16 neii2 22037 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦𝐽 ({𝑃} ⊆ 𝑦𝑦𝑁))
178, 16sylan 583 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦𝐽 ({𝑃} ⊆ 𝑦𝑦𝑁))
18 pweq 4546 . . . . . . . . . . 11 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
1918ineq2d 4144 . . . . . . . . . 10 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
2019neeq1d 3003 . . . . . . . . 9 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
2120raleqbi1dv 3332 . . . . . . . 8 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
2221, 4elrab2 3620 . . . . . . 7 (𝑦𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
23 simprrr 782 . . . . . . . . . . . . 13 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → 𝑦𝑁)
2423sspwd 4545 . . . . . . . . . . . 12 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → 𝒫 𝑦 ⊆ 𝒫 𝑁)
25 sslin 4166 . . . . . . . . . . . 12 (𝒫 𝑦 ⊆ 𝒫 𝑁 → ((𝐹𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹𝑃) ∩ 𝒫 𝑁))
2624, 25syl 17 . . . . . . . . . . 11 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → ((𝐹𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹𝑃) ∩ 𝒫 𝑁))
27 simprrl 781 . . . . . . . . . . . . 13 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → {𝑃} ⊆ 𝑦)
28 snssg 4715 . . . . . . . . . . . . . 14 (𝑃𝑋 → (𝑃𝑦 ↔ {𝑃} ⊆ 𝑦))
2928ad3antlr 731 . . . . . . . . . . . . 13 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → (𝑃𝑦 ↔ {𝑃} ⊆ 𝑦))
3027, 29mpbird 260 . . . . . . . . . . . 12 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → 𝑃𝑦)
31 fveq2 6739 . . . . . . . . . . . . . . 15 (𝑥 = 𝑃 → (𝐹𝑥) = (𝐹𝑃))
3231ineq1d 4143 . . . . . . . . . . . . . 14 (𝑥 = 𝑃 → ((𝐹𝑥) ∩ 𝒫 𝑦) = ((𝐹𝑃) ∩ 𝒫 𝑦))
3332neeq1d 3003 . . . . . . . . . . . . 13 (𝑥 = 𝑃 → (((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅))
3433rspcv 3547 . . . . . . . . . . . 12 (𝑃𝑦 → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅))
3530, 34syl 17 . . . . . . . . . . 11 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅))
36 ssn0 4332 . . . . . . . . . . 11 ((((𝐹𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹𝑃) ∩ 𝒫 𝑁) ∧ ((𝐹𝑃) ∩ 𝒫 𝑦) ≠ ∅) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)
3726, 35, 36syl6an 684 . . . . . . . . . 10 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦𝑦𝑁))) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅))
3837expr 460 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (({𝑃} ⊆ 𝑦𝑦𝑁) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
3938com23 86 . . . . . . . 8 ((((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → (({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
4039expimpd 457 . . . . . . 7 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) → (({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
4122, 40syl5bi 245 . . . . . 6 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑦𝐽 → (({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
4241rexlimdv 3212 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (∃𝑦𝐽 ({𝑃} ⊆ 𝑦𝑦𝑁) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅))
4317, 42mpd 15 . . . 4 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)
4415, 43jca 515 . . 3 (((𝜑𝑃𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅))
4544ex 416 . 2 ((𝜑𝑃𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) → (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
46 n0 4278 . . . 4 (((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁))
47 elin 3899 . . . . . 6 (𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁) ↔ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))
48 simprl 771 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁𝑋)
4913ad2antrr 726 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 = 𝐽)
5048, 49sseqtrd 3958 . . . . . . . 8 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 𝐽)
511ad2antrr 726 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋𝑉)
522ad2antrr 726 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
53 simpll 767 . . . . . . . . . 10 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝜑)
5453, 3sylan 583 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
55 neibastop1.5 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
5653, 55sylan 583 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
57 neibastop1.6 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
5853, 57sylan 583 . . . . . . . . 9 ((((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
59 simplr 769 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃𝑋)
60 simprrl 781 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ (𝐹𝑃))
61 simprrr 782 . . . . . . . . . 10 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ 𝒫 𝑁)
6261elpwid 4541 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠𝑁)
63 fveq2 6739 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → (𝐹𝑛) = (𝐹𝑥))
6463ineq1d 4143 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → ((𝐹𝑛) ∩ 𝒫 𝑏) = ((𝐹𝑥) ∩ 𝒫 𝑏))
6564cbviunv 4966 . . . . . . . . . . . . . 14 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏) = 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑏)
66 pweq 4546 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧)
6766ineq2d 4144 . . . . . . . . . . . . . . 15 (𝑏 = 𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑏) = ((𝐹𝑥) ∩ 𝒫 𝑧))
6867iuneq2d 4950 . . . . . . . . . . . . . 14 (𝑏 = 𝑧 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑏) = 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
6965, 68syl5eq 2792 . . . . . . . . . . . . 13 (𝑏 = 𝑧 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏) = 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
7069cbviunv 4966 . . . . . . . . . . . 12 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏) = 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)
7170mpteq2i 5164 . . . . . . . . . . 11 (𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
72 rdgeq1 8171 . . . . . . . . . . 11 ((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)) → rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑠}))
7371, 72ax-mp 5 . . . . . . . . . 10 rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑠})
7473reseq1i 5865 . . . . . . . . 9 (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω) = (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑠}) ↾ ω)
75 pweq 4546 . . . . . . . . . . . . . 14 (𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓)
7675ineq2d 4144 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → ((𝐹𝑤) ∩ 𝒫 𝑔) = ((𝐹𝑤) ∩ 𝒫 𝑓))
7776neeq1d 3003 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅))
7877cbvrexvw 3374 . . . . . . . . . . 11 (∃𝑔 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅)
79 fveq2 6739 . . . . . . . . . . . . . 14 (𝑤 = 𝑦 → (𝐹𝑤) = (𝐹𝑦))
8079ineq1d 4143 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → ((𝐹𝑤) ∩ 𝒫 𝑓) = ((𝐹𝑦) ∩ 𝒫 𝑓))
8180neeq1d 3003 . . . . . . . . . . . 12 (𝑤 = 𝑦 → (((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
8281rexbidv 3226 . . . . . . . . . . 11 (𝑤 = 𝑦 → (∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
8378, 82syl5bb 286 . . . . . . . . . 10 (𝑤 = 𝑦 → (∃𝑔 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
8483cbvrabv 3417 . . . . . . . . 9 {𝑤𝑋 ∣ ∃𝑔 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑤) ∩ 𝒫 𝑔) ≠ ∅} = {𝑦𝑋 ∣ ∃𝑓 ran (rec((𝑎 ∈ V ↦ 𝑏𝑎 𝑛𝑋 ((𝐹𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅}
8551, 52, 54, 4, 56, 58, 59, 48, 60, 62, 74, 84neibastop2lem 34320 . . . . . . . 8 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
867ad2antrr 726 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐽 ∈ Top)
8759, 49eleqtrd 2842 . . . . . . . . 9 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 𝐽)
889isneip 22034 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑃 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 𝐽 ∧ ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))))
8986, 87, 88syl2anc 587 . . . . . . . 8 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 𝐽 ∧ ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))))
9050, 85, 89mpbir2and 713 . . . . . . 7 (((𝜑𝑃𝑋) ∧ (𝑁𝑋 ∧ (𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
9190expr 460 . . . . . 6 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → ((𝑠 ∈ (𝐹𝑃) ∧ 𝑠 ∈ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9247, 91syl5bi 245 . . . . 5 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → (𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9392exlimdv 1941 . . . 4 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → (∃𝑠 𝑠 ∈ ((𝐹𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9446, 93syl5bi 245 . . 3 (((𝜑𝑃𝑋) ∧ 𝑁𝑋) → (((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅ → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9594expimpd 457 . 2 ((𝜑𝑃𝑋) → ((𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
9645, 95impbid 215 1 ((𝜑𝑃𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wex 1787  wcel 2112  wne 2943  wral 3064  wrex 3065  {crab 3068  Vcvv 3423  cdif 3880  cin 3882  wss 3883  c0 4254  𝒫 cpw 4530  {csn 4558   cuni 4836   ciun 4921  cmpt 5152  ran crn 5570  cres 5571  wf 6397  cfv 6401  ωcom 7666  reccrdg 8169  Topctop 21822  TopOnctopon 21839  neicnei 22026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-om 7667  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-top 21823  df-topon 21840  df-nei 22027
This theorem is referenced by:  neibastop3  34322
  Copyright terms: Public domain W3C validator