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 32329
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 477 . . . . . . . . 9 ((𝜑𝑦𝐽) → 𝑦𝐽)
2 neibastop1.4 . . . . . . . . . 10 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
3 ssrab2 3679 . . . . . . . . . 10 {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅} ⊆ 𝒫 𝑋
42, 3eqsstri 3627 . . . . . . . . 9 𝐽 ⊆ 𝒫 𝑋
51, 4syl6ss 3607 . . . . . . . 8 ((𝜑𝑦𝐽) → 𝑦 ⊆ 𝒫 𝑋)
6 sspwuni 4602 . . . . . . . 8 (𝑦 ⊆ 𝒫 𝑋 𝑦𝑋)
75, 6sylib 208 . . . . . . 7 ((𝜑𝑦𝐽) → 𝑦𝑋)
8 vuniex 6939 . . . . . . . 8 𝑦 ∈ V
98elpw 4155 . . . . . . 7 ( 𝑦 ∈ 𝒫 𝑋 𝑦𝑋)
107, 9sylibr 224 . . . . . 6 ((𝜑𝑦𝐽) → 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4431 . . . . . . . 8 (𝑥 𝑦 ↔ ∃𝑧𝑦 𝑥𝑧)
12 elssuni 4458 . . . . . . . . . . . . 13 (𝑧𝑦𝑧 𝑦)
1312ad2antrl 763 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧 𝑦)
14 sspwb 4908 . . . . . . . . . . . 12 (𝑧 𝑦 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑦)
1513, 14sylib 208 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝒫 𝑧 ⊆ 𝒫 𝑦)
16 sslin 3831 . . . . . . . . . . 11 (𝒫 𝑧 ⊆ 𝒫 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
1715, 16syl 17 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
181sselda 3595 . . . . . . . . . . . . 13 (((𝜑𝑦𝐽) ∧ 𝑧𝑦) → 𝑧𝐽)
1918adantrr 752 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧𝐽)
20 pweq 4152 . . . . . . . . . . . . . . . . 17 (𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧)
2120ineq2d 3806 . . . . . . . . . . . . . . . 16 (𝑜 = 𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑧))
2221neeq1d 2850 . . . . . . . . . . . . . . 15 (𝑜 = 𝑧 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2322raleqbi1dv 3141 . . . . . . . . . . . . . 14 (𝑜 = 𝑧 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2423, 2elrab2 3360 . . . . . . . . . . . . 13 (𝑧𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2524simprbi 480 . . . . . . . . . . . 12 (𝑧𝐽 → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
2619, 25syl 17 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
27 simprr 795 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑥𝑧)
28 rsp 2926 . . . . . . . . . . 11 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → (𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2926, 27, 28sylc 65 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
30 ssn0 3967 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3117, 29, 30syl2anc 692 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3231rexlimdvaa 3028 . . . . . . . 8 ((𝜑𝑦𝐽) → (∃𝑧𝑦 𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3311, 32syl5bi 232 . . . . . . 7 ((𝜑𝑦𝐽) → (𝑥 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3433ralrimiv 2962 . . . . . 6 ((𝜑𝑦𝐽) → ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
35 pweq 4152 . . . . . . . . . 10 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
3635ineq2d 3806 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
3736neeq1d 2850 . . . . . . . 8 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3837raleqbi1dv 3141 . . . . . . 7 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3938, 2elrab2 3360 . . . . . 6 ( 𝑦𝐽 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4010, 34, 39sylanbrc 697 . . . . 5 ((𝜑𝑦𝐽) → 𝑦𝐽)
4140ex 450 . . . 4 (𝜑 → (𝑦𝐽 𝑦𝐽))
4241alrimiv 1853 . . 3 (𝜑 → ∀𝑦(𝑦𝐽 𝑦𝐽))
43 pweq 4152 . . . . . . . . . . 11 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
4443ineq2d 3806 . . . . . . . . . 10 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
4544neeq1d 2850 . . . . . . . . 9 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4645raleqbi1dv 3141 . . . . . . . 8 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4746, 2elrab2 3360 . . . . . . 7 (𝑦𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4847, 24anbi12i 732 . . . . . 6 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
49 an4 864 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
5048, 49bitri 264 . . . . 5 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
51 inss1 3825 . . . . . . . . . 10 (𝑦𝑧) ⊆ 𝑦
52 elpwi 4159 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
5351, 52syl5ss 3606 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 → (𝑦𝑧) ⊆ 𝑋)
5453ad2antrl 763 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (𝑦𝑧) ⊆ 𝑋)
5554adantrr 752 . . . . . . 7 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ⊆ 𝑋)
56 vex 3198 . . . . . . . . 9 𝑦 ∈ V
5756inex1 4790 . . . . . . . 8 (𝑦𝑧) ∈ V
5857elpw 4155 . . . . . . 7 ((𝑦𝑧) ∈ 𝒫 𝑋 ↔ (𝑦𝑧) ⊆ 𝑋)
5955, 58sylibr 224 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝒫 𝑋)
60 ssralv 3658 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑦 → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
6151, 60ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
62 inss2 3826 . . . . . . . . . . 11 (𝑦𝑧) ⊆ 𝑧
63 ssralv 3658 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑧 → (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6462, 63ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
6561, 64anim12i 589 . . . . . . . . 9 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
66 r19.26 3060 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6765, 66sylibr 224 . . . . . . . 8 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
68 n0 3923 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
69 n0 3923 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7068, 69anbi12i 732 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
71 eeanv 2180 . . . . . . . . . . 11 (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
72 inss2 3826 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ 𝒫 𝑦
73 simprl 793 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
7472, 73sseldi 3593 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ 𝒫 𝑦)
7574elpwid 4161 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣𝑦)
76 inss2 3826 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
77 simprr 795 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7876, 77sseldi 3593 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
7978elpwid 4161 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤𝑧)
80 ss2in 3832 . . . . . . . . . . . . . . . . 17 ((𝑣𝑦𝑤𝑧) → (𝑣𝑤) ⊆ (𝑦𝑧))
8175, 79, 80syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑣𝑤) ⊆ (𝑦𝑧))
82 sspwb 4908 . . . . . . . . . . . . . . . 16 ((𝑣𝑤) ⊆ (𝑦𝑧) ↔ 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
8381, 82sylib 208 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
84 sslin 3831 . . . . . . . . . . . . . . 15 (𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
8583, 84syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
86 simplll 797 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝜑)
8754ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑦𝑧) ⊆ 𝑋)
88 simplr 791 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ (𝑦𝑧))
8987, 88sseldd 3596 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥𝑋)
90 inss1 3825 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ (𝐹𝑥)
9190, 73sseldi 3593 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ (𝐹𝑥))
92 inss1 3825 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ (𝐹𝑥)
9392, 77sseldi 3593 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ (𝐹𝑥))
94 neibastop1.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
9586, 89, 91, 93, 94syl13anc 1326 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
96 ssn0 3967 . . . . . . . . . . . . . 14 ((((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ∧ ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9785, 95, 96syl2anc 692 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9897ex 450 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9998exlimdvv 1860 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10071, 99syl5bir 233 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10170, 100syl5bi 232 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
102101ralimdva 2959 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10367, 102syl5 34 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
104103impr 648 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
105 pweq 4152 . . . . . . . . . 10 (𝑜 = (𝑦𝑧) → 𝒫 𝑜 = 𝒫 (𝑦𝑧))
106105ineq2d 3806 . . . . . . . . 9 (𝑜 = (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
107106neeq1d 2850 . . . . . . . 8 (𝑜 = (𝑦𝑧) → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
108107raleqbi1dv 3141 . . . . . . 7 (𝑜 = (𝑦𝑧) → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
109108, 2elrab2 3360 . . . . . 6 ((𝑦𝑧) ∈ 𝐽 ↔ ((𝑦𝑧) ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
11059, 104, 109sylanbrc 697 . . . . 5 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝐽)
11150, 110sylan2b 492 . . . 4 ((𝜑 ∧ (𝑦𝐽𝑧𝐽)) → (𝑦𝑧) ∈ 𝐽)
112111ralrimivva 2968 . . 3 (𝜑 → ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)
113 neibastop1.1 . . . . . 6 (𝜑𝑋𝑉)
114 sspwuni 4602 . . . . . . . 8 (𝐽 ⊆ 𝒫 𝑋 𝐽𝑋)
1154, 114mpbi 220 . . . . . . 7 𝐽𝑋
116115a1i 11 . . . . . 6 (𝜑 𝐽𝑋)
117113, 116ssexd 4796 . . . . 5 (𝜑 𝐽 ∈ V)
118 uniexb 6958 . . . . 5 (𝐽 ∈ V ↔ 𝐽 ∈ V)
119117, 118sylibr 224 . . . 4 (𝜑𝐽 ∈ V)
120 istopg 20681 . . . 4 (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
121119, 120syl 17 . . 3 (𝜑 → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
12242, 112, 121mpbir2and 956 . 2 (𝜑𝐽 ∈ Top)
123 pwidg 4164 . . . . . 6 (𝑋𝑉𝑋 ∈ 𝒫 𝑋)
124113, 123syl 17 . . . . 5 (𝜑𝑋 ∈ 𝒫 𝑋)
125 neibastop1.2 . . . . . . . . . 10 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
126125ffvelrnda 6345 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}))
127 eldifi 3724 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝒫 𝑋)
128 elpwi 4159 . . . . . . . . 9 ((𝐹𝑥) ∈ 𝒫 𝒫 𝑋 → (𝐹𝑥) ⊆ 𝒫 𝑋)
129126, 127, 1283syl 18 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐹𝑥) ⊆ 𝒫 𝑋)
130 df-ss 3581 . . . . . . . 8 ((𝐹𝑥) ⊆ 𝒫 𝑋 ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
131129, 130sylib 208 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
132 eldifsni 4311 . . . . . . . 8 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
133126, 132syl 17 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ≠ ∅)
134131, 133eqnetrd 2858 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
135134ralrimiva 2963 . . . . 5 (𝜑 → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
136 pweq 4152 . . . . . . . . 9 (𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋)
137136ineq2d 3806 . . . . . . . 8 (𝑜 = 𝑋 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑋))
138137neeq1d 2850 . . . . . . 7 (𝑜 = 𝑋 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
139138raleqbi1dv 3141 . . . . . 6 (𝑜 = 𝑋 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
140139, 2elrab2 3360 . . . . 5 (𝑋𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
141124, 135, 140sylanbrc 697 . . . 4 (𝜑𝑋𝐽)
142 elssuni 4458 . . . 4 (𝑋𝐽𝑋 𝐽)
143141, 142syl 17 . . 3 (𝜑𝑋 𝐽)
144143, 116eqssd 3612 . 2 (𝜑𝑋 = 𝐽)
145 istopon 20698 . 2 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
146122, 144, 145sylanbrc 697 1 (𝜑𝐽 ∈ (TopOn‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1479   = wceq 1481  wex 1702  wcel 1988  wne 2791  wral 2909  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168   cuni 4427  wf 5872  cfv 5876  Topctop 20679  TopOnctopon 20696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884  df-top 20680  df-topon 20697
This theorem is referenced by:  neibastop2  32331  neibastop3  32332
  Copyright terms: Public domain W3C validator