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

Theorem neibastop1 31358
Description: A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard's General Topology. (Contributed by Jeff Hankins, 8-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
neibastop1.1 (𝜑𝑋𝑉)
neibastop1.2 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
neibastop1.3 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
neibastop1.4 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
Assertion
Ref Expression
neibastop1 (𝜑𝐽 ∈ (TopOn‘𝑋))
Distinct variable groups:   𝑥,𝑣,𝐽   𝑣,𝑜,𝑤,𝑥,𝐹   𝜑,𝑜,𝑣,𝑤,𝑥   𝑜,𝑋,𝑣,𝑤,𝑥
Allowed substitution hints:   𝐽(𝑤,𝑜)   𝑉(𝑥,𝑤,𝑣,𝑜)

Proof of Theorem neibastop1
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 475 . . . . . . . . 9 ((𝜑𝑦𝐽) → 𝑦𝐽)
2 neibastop1.4 . . . . . . . . . 10 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
3 ssrab2 3554 . . . . . . . . . 10 {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅} ⊆ 𝒫 𝑋
42, 3eqsstri 3502 . . . . . . . . 9 𝐽 ⊆ 𝒫 𝑋
51, 4syl6ss 3484 . . . . . . . 8 ((𝜑𝑦𝐽) → 𝑦 ⊆ 𝒫 𝑋)
6 sspwuni 4445 . . . . . . . 8 (𝑦 ⊆ 𝒫 𝑋 𝑦𝑋)
75, 6sylib 206 . . . . . . 7 ((𝜑𝑦𝐽) → 𝑦𝑋)
8 vuniex 6728 . . . . . . . 8 𝑦 ∈ V
98elpw 4017 . . . . . . 7 ( 𝑦 ∈ 𝒫 𝑋 𝑦𝑋)
107, 9sylibr 222 . . . . . 6 ((𝜑𝑦𝐽) → 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4274 . . . . . . . 8 (𝑥 𝑦 ↔ ∃𝑧𝑦 𝑥𝑧)
12 elssuni 4301 . . . . . . . . . . . . 13 (𝑧𝑦𝑧 𝑦)
1312ad2antrl 759 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧 𝑦)
14 sspwb 4742 . . . . . . . . . . . 12 (𝑧 𝑦 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑦)
1513, 14sylib 206 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝒫 𝑧 ⊆ 𝒫 𝑦)
16 sslin 3704 . . . . . . . . . . 11 (𝒫 𝑧 ⊆ 𝒫 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
1715, 16syl 17 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
181sselda 3472 . . . . . . . . . . . . 13 (((𝜑𝑦𝐽) ∧ 𝑧𝑦) → 𝑧𝐽)
1918adantrr 748 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧𝐽)
20 pweq 4014 . . . . . . . . . . . . . . . . 17 (𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧)
2120ineq2d 3679 . . . . . . . . . . . . . . . 16 (𝑜 = 𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑧))
2221neeq1d 2745 . . . . . . . . . . . . . . 15 (𝑜 = 𝑧 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2322raleqbi1dv 3027 . . . . . . . . . . . . . 14 (𝑜 = 𝑧 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2423, 2elrab2 3237 . . . . . . . . . . . . 13 (𝑧𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2524simprbi 478 . . . . . . . . . . . 12 (𝑧𝐽 → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
2619, 25syl 17 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
27 simprr 791 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑥𝑧)
28 rsp 2817 . . . . . . . . . . 11 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → (𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2926, 27, 28sylc 62 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
30 ssn0 3831 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3117, 29, 30syl2anc 690 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3231rexlimdvaa 2918 . . . . . . . 8 ((𝜑𝑦𝐽) → (∃𝑧𝑦 𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3311, 32syl5bi 230 . . . . . . 7 ((𝜑𝑦𝐽) → (𝑥 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3433ralrimiv 2852 . . . . . 6 ((𝜑𝑦𝐽) → ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
35 pweq 4014 . . . . . . . . . 10 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
3635ineq2d 3679 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
3736neeq1d 2745 . . . . . . . 8 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3837raleqbi1dv 3027 . . . . . . 7 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3938, 2elrab2 3237 . . . . . 6 ( 𝑦𝐽 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4010, 34, 39sylanbrc 694 . . . . 5 ((𝜑𝑦𝐽) → 𝑦𝐽)
4140ex 448 . . . 4 (𝜑 → (𝑦𝐽 𝑦𝐽))
4241alrimiv 1808 . . 3 (𝜑 → ∀𝑦(𝑦𝐽 𝑦𝐽))
43 pweq 4014 . . . . . . . . . . 11 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
4443ineq2d 3679 . . . . . . . . . 10 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
4544neeq1d 2745 . . . . . . . . 9 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4645raleqbi1dv 3027 . . . . . . . 8 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4746, 2elrab2 3237 . . . . . . 7 (𝑦𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4847, 24anbi12i 728 . . . . . 6 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
49 an4 860 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
5048, 49bitri 262 . . . . 5 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
51 inss1 3698 . . . . . . . . . 10 (𝑦𝑧) ⊆ 𝑦
52 elpwi 4020 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
5351, 52syl5ss 3483 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 → (𝑦𝑧) ⊆ 𝑋)
5453ad2antrl 759 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (𝑦𝑧) ⊆ 𝑋)
5554adantrr 748 . . . . . . 7 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ⊆ 𝑋)
56 vex 3080 . . . . . . . . 9 𝑦 ∈ V
5756inex1 4626 . . . . . . . 8 (𝑦𝑧) ∈ V
5857elpw 4017 . . . . . . 7 ((𝑦𝑧) ∈ 𝒫 𝑋 ↔ (𝑦𝑧) ⊆ 𝑋)
5955, 58sylibr 222 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝒫 𝑋)
60 ssralv 3533 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑦 → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
6151, 60ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
62 inss2 3699 . . . . . . . . . . 11 (𝑦𝑧) ⊆ 𝑧
63 ssralv 3533 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑧 → (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6462, 63ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
6561, 64anim12i 587 . . . . . . . . 9 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
66 r19.26 2950 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6765, 66sylibr 222 . . . . . . . 8 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
68 n0 3793 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
69 n0 3793 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7068, 69anbi12i 728 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
71 eeanv 2125 . . . . . . . . . . 11 (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
72 inss2 3699 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ 𝒫 𝑦
73 simprl 789 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
7472, 73sseldi 3470 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ 𝒫 𝑦)
7574elpwid 4021 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣𝑦)
76 inss2 3699 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
77 simprr 791 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7876, 77sseldi 3470 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
7978elpwid 4021 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤𝑧)
80 ss2in 3705 . . . . . . . . . . . . . . . . 17 ((𝑣𝑦𝑤𝑧) → (𝑣𝑤) ⊆ (𝑦𝑧))
8175, 79, 80syl2anc 690 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑣𝑤) ⊆ (𝑦𝑧))
82 sspwb 4742 . . . . . . . . . . . . . . . 16 ((𝑣𝑤) ⊆ (𝑦𝑧) ↔ 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
8381, 82sylib 206 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
84 sslin 3704 . . . . . . . . . . . . . . 15 (𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
8583, 84syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
86 simplll 793 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝜑)
8754ad2antrr 757 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑦𝑧) ⊆ 𝑋)
88 simplr 787 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ (𝑦𝑧))
8987, 88sseldd 3473 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥𝑋)
90 inss1 3698 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ (𝐹𝑥)
9190, 73sseldi 3470 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ (𝐹𝑥))
92 inss1 3698 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ (𝐹𝑥)
9392, 77sseldi 3470 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ (𝐹𝑥))
94 neibastop1.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
9586, 89, 91, 93, 94syl13anc 1319 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
96 ssn0 3831 . . . . . . . . . . . . . 14 ((((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ∧ ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9785, 95, 96syl2anc 690 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9897ex 448 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9998exlimdvv 1815 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10071, 99syl5bir 231 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10170, 100syl5bi 230 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
102101ralimdva 2849 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10367, 102syl5 33 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
104103impr 646 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
105 pweq 4014 . . . . . . . . . 10 (𝑜 = (𝑦𝑧) → 𝒫 𝑜 = 𝒫 (𝑦𝑧))
106105ineq2d 3679 . . . . . . . . 9 (𝑜 = (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
107106neeq1d 2745 . . . . . . . 8 (𝑜 = (𝑦𝑧) → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
108107raleqbi1dv 3027 . . . . . . 7 (𝑜 = (𝑦𝑧) → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
109108, 2elrab2 3237 . . . . . 6 ((𝑦𝑧) ∈ 𝐽 ↔ ((𝑦𝑧) ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
11059, 104, 109sylanbrc 694 . . . . 5 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝐽)
11150, 110sylan2b 490 . . . 4 ((𝜑 ∧ (𝑦𝐽𝑧𝐽)) → (𝑦𝑧) ∈ 𝐽)
112111ralrimivva 2858 . . 3 (𝜑 → ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)
113 neibastop1.1 . . . . . 6 (𝜑𝑋𝑉)
114 sspwuni 4445 . . . . . . . 8 (𝐽 ⊆ 𝒫 𝑋 𝐽𝑋)
1154, 114mpbi 218 . . . . . . 7 𝐽𝑋
116115a1i 11 . . . . . 6 (𝜑 𝐽𝑋)
117113, 116ssexd 4632 . . . . 5 (𝜑 𝐽 ∈ V)
118 uniexb 6742 . . . . 5 (𝐽 ∈ V ↔ 𝐽 ∈ V)
119117, 118sylibr 222 . . . 4 (𝜑𝐽 ∈ V)
120 istopg 20428 . . . 4 (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
121119, 120syl 17 . . 3 (𝜑 → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
12242, 112, 121mpbir2and 958 . 2 (𝜑𝐽 ∈ Top)
123 pwidg 4024 . . . . . 6 (𝑋𝑉𝑋 ∈ 𝒫 𝑋)
124113, 123syl 17 . . . . 5 (𝜑𝑋 ∈ 𝒫 𝑋)
125 neibastop1.2 . . . . . . . . . 10 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
126125ffvelrnda 6151 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}))
127 eldifi 3598 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝒫 𝑋)
128 elpwi 4020 . . . . . . . . 9 ((𝐹𝑥) ∈ 𝒫 𝒫 𝑋 → (𝐹𝑥) ⊆ 𝒫 𝑋)
129126, 127, 1283syl 18 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐹𝑥) ⊆ 𝒫 𝑋)
130 df-ss 3458 . . . . . . . 8 ((𝐹𝑥) ⊆ 𝒫 𝑋 ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
131129, 130sylib 206 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
132 eldifsni 4164 . . . . . . . 8 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
133126, 132syl 17 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ≠ ∅)
134131, 133eqnetrd 2753 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
135134ralrimiva 2853 . . . . 5 (𝜑 → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
136 pweq 4014 . . . . . . . . 9 (𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋)
137136ineq2d 3679 . . . . . . . 8 (𝑜 = 𝑋 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑋))
138137neeq1d 2745 . . . . . . 7 (𝑜 = 𝑋 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
139138raleqbi1dv 3027 . . . . . 6 (𝑜 = 𝑋 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
140139, 2elrab2 3237 . . . . 5 (𝑋𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
141124, 135, 140sylanbrc 694 . . . 4 (𝜑𝑋𝐽)
142 elssuni 4301 . . . 4 (𝑋𝐽𝑋 𝐽)
143141, 142syl 17 . . 3 (𝜑𝑋 𝐽)
144143, 116eqssd 3489 . 2 (𝜑𝑋 = 𝐽)
145 istopon 20443 . 2 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
146122, 144, 145sylanbrc 694 1 (𝜑𝐽 ∈ (TopOn‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030  wal 1472   = wceq 1474  wex 1694  wcel 1938  wne 2684  wral 2800  wrex 2801  {crab 2804  Vcvv 3077  cdif 3441  cin 3443  wss 3444  c0 3777  𝒫 cpw 4011  {csn 4028   cuni 4270  wf 5685  cfv 5689  Topctop 20420  TopOnctopon 20421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-fv 5697  df-top 20424  df-topon 20426
This theorem is referenced by:  neibastop2  31360  neibastop3  31361
  Copyright terms: Public domain W3C validator