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 35239
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 485 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ 𝑦 βŠ† 𝐽)
2 neibastop1.4 . . . . . . . . . 10 𝐽 = {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…}
3 ssrab2 4077 . . . . . . . . . 10 {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…} βŠ† 𝒫 𝑋
42, 3eqsstri 4016 . . . . . . . . 9 𝐽 βŠ† 𝒫 𝑋
51, 4sstrdi 3994 . . . . . . . 8 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ 𝑦 βŠ† 𝒫 𝑋)
6 sspwuni 5103 . . . . . . . 8 (𝑦 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝑦 βŠ† 𝑋)
75, 6sylib 217 . . . . . . 7 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 βŠ† 𝑋)
8 vuniex 7728 . . . . . . . 8 βˆͺ 𝑦 ∈ V
98elpw 4606 . . . . . . 7 (βˆͺ 𝑦 ∈ 𝒫 𝑋 ↔ βˆͺ 𝑦 βŠ† 𝑋)
107, 9sylibr 233 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4912 . . . . . . . 8 (π‘₯ ∈ βˆͺ 𝑦 ↔ βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧)
12 elssuni 4941 . . . . . . . . . . . . 13 (𝑧 ∈ 𝑦 β†’ 𝑧 βŠ† βˆͺ 𝑦)
1312ad2antrl 726 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 βŠ† βˆͺ 𝑦)
1413sspwd 4615 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦)
15 sslin 4234 . . . . . . . . . . 11 (𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
1614, 15syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
171sselda 3982 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐽)
1817adantrr 715 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐽)
19 pweq 4616 . . . . . . . . . . . . . . . . 17 (π‘œ = 𝑧 β†’ 𝒫 π‘œ = 𝒫 𝑧)
2019ineq2d 4212 . . . . . . . . . . . . . . . 16 (π‘œ = 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
2120neeq1d 3000 . . . . . . . . . . . . . . 15 (π‘œ = 𝑧 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2221raleqbi1dv 3333 . . . . . . . . . . . . . 14 (π‘œ = 𝑧 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2322, 2elrab2 3686 . . . . . . . . . . . . 13 (𝑧 ∈ 𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2423simprbi 497 . . . . . . . . . . . 12 (𝑧 ∈ 𝐽 β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
2518, 24syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
26 simprr 771 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ π‘₯ ∈ 𝑧)
27 rsp 3244 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ (π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2825, 26, 27sylc 65 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
29 ssn0 4400 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3016, 28, 29syl2anc 584 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3130rexlimdvaa 3156 . . . . . . . 8 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3211, 31biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (π‘₯ ∈ βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3332ralrimiv 3145 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
34 pweq 4616 . . . . . . . . . 10 (π‘œ = βˆͺ 𝑦 β†’ 𝒫 π‘œ = 𝒫 βˆͺ 𝑦)
3534ineq2d 4212 . . . . . . . . 9 (π‘œ = βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
3635neeq1d 3000 . . . . . . . 8 (π‘œ = βˆͺ 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3736raleqbi1dv 3333 . . . . . . 7 (π‘œ = βˆͺ 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3837, 2elrab2 3686 . . . . . 6 (βˆͺ 𝑦 ∈ 𝐽 ↔ (βˆͺ 𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3910, 33, 38sylanbrc 583 . . . . 5 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝐽)
4039ex 413 . . . 4 (πœ‘ β†’ (𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
4140alrimiv 1930 . . 3 (πœ‘ β†’ βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
42 pweq 4616 . . . . . . . . . . 11 (π‘œ = 𝑦 β†’ 𝒫 π‘œ = 𝒫 𝑦)
4342ineq2d 4212 . . . . . . . . . 10 (π‘œ = 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
4443neeq1d 3000 . . . . . . . . 9 (π‘œ = 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4544raleqbi1dv 3333 . . . . . . . 8 (π‘œ = 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4645, 2elrab2 3686 . . . . . . 7 (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4746, 23anbi12i 627 . . . . . 6 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
48 an4 654 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
4947, 48bitri 274 . . . . 5 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
50 inss1 4228 . . . . . . . . . 10 (𝑦 ∩ 𝑧) βŠ† 𝑦
51 elpwi 4609 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋 β†’ 𝑦 βŠ† 𝑋)
5250, 51sstrid 3993 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5352ad2antrl 726 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5453adantrr 715 . . . . . . 7 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
55 vex 3478 . . . . . . . . 9 𝑦 ∈ V
5655inex1 5317 . . . . . . . 8 (𝑦 ∩ 𝑧) ∈ V
5756elpw 4606 . . . . . . 7 ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ↔ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5854, 57sylibr 233 . . . . . 6 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) ∈ 𝒫 𝑋)
59 ssralv 4050 . . . . . . . . . . 11 ((𝑦 ∩ 𝑧) βŠ† 𝑦 β†’ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
6050, 59ax-mp 5 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…)
61 inss2 4229 . . . . . . . . . . 11 (𝑦 ∩ 𝑧) βŠ† 𝑧
62 ssralv 4050 . . . . . . . . . . 11 ((𝑦 ∩ 𝑧) βŠ† 𝑧 β†’ (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
6361, 62ax-mp 5 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
6460, 63anim12i 613 . . . . . . . . 9 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
65 r19.26 3111 . . . . . . . . 9 (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
6664, 65sylibr 233 . . . . . . . 8 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
67 n0 4346 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
68 n0 4346 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… ↔ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
6967, 68anbi12i 627 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
70 exdistrv 1959 . . . . . . . . . . 11 (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
71 inss2 4229 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) βŠ† 𝒫 𝑦
72 simprl 769 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
7371, 72sselid 3980 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ 𝒫 𝑦)
7473elpwid 4611 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 βŠ† 𝑦)
75 inss2 4229 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 𝑧
76 simprr 771 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
7775, 76sselid 3980 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ 𝒫 𝑧)
7877elpwid 4611 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 βŠ† 𝑧)
79 ss2in 4236 . . . . . . . . . . . . . . . . 17 ((𝑣 βŠ† 𝑦 ∧ 𝑀 βŠ† 𝑧) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8074, 78, 79syl2anc 584 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8180sspwd 4615 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧))
82 sslin 4234 . . . . . . . . . . . . . . 15 (𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
8381, 82syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
84 simplll 773 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ πœ‘)
8553ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
86 simplr 767 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ π‘₯ ∈ (𝑦 ∩ 𝑧))
8785, 86sseldd 3983 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ π‘₯ ∈ 𝑋)
88 inss1 4228 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) βŠ† (πΉβ€˜π‘₯)
8988, 72sselid 3980 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ (πΉβ€˜π‘₯))
90 inss1 4228 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† (πΉβ€˜π‘₯)
9190, 76sselid 3980 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ (πΉβ€˜π‘₯))
92 neibastop1.3 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯) ∧ 𝑀 ∈ (πΉβ€˜π‘₯))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
9384, 87, 89, 91, 92syl13anc 1372 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
94 ssn0 4400 . . . . . . . . . . . . . 14 ((((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9583, 93, 94syl2anc 584 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9695ex 413 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9796exlimdvv 1937 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9870, 97biimtrrid 242 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9969, 98biimtrid 241 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10099ralimdva 3167 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10166, 100syl5 34 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
102101impr 455 . . . . . 6 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
103 pweq 4616 . . . . . . . . . 10 (π‘œ = (𝑦 ∩ 𝑧) β†’ 𝒫 π‘œ = 𝒫 (𝑦 ∩ 𝑧))
104103ineq2d 4212 . . . . . . . . 9 (π‘œ = (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
105104neeq1d 3000 . . . . . . . 8 (π‘œ = (𝑦 ∩ 𝑧) β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
106105raleqbi1dv 3333 . . . . . . 7 (π‘œ = (𝑦 ∩ 𝑧) β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
107106, 2elrab2 3686 . . . . . 6 ((𝑦 ∩ 𝑧) ∈ 𝐽 ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10858, 102, 107sylanbrc 583 . . . . 5 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
10949, 108sylan2b 594 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽)) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
110109ralrimivva 3200 . . 3 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)
111 neibastop1.1 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ 𝑉)
112 sspwuni 5103 . . . . . . . 8 (𝐽 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝐽 βŠ† 𝑋)
1134, 112mpbi 229 . . . . . . 7 βˆͺ 𝐽 βŠ† 𝑋
114113a1i 11 . . . . . 6 (πœ‘ β†’ βˆͺ 𝐽 βŠ† 𝑋)
115111, 114ssexd 5324 . . . . 5 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
116 uniexb 7750 . . . . 5 (𝐽 ∈ V ↔ βˆͺ 𝐽 ∈ V)
117115, 116sylibr 233 . . . 4 (πœ‘ β†’ 𝐽 ∈ V)
118 istopg 22396 . . . 4 (𝐽 ∈ V β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
119117, 118syl 17 . . 3 (πœ‘ β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
12041, 110, 119mpbir2and 711 . 2 (πœ‘ β†’ 𝐽 ∈ Top)
121 pwidg 4622 . . . . . 6 (𝑋 ∈ 𝑉 β†’ 𝑋 ∈ 𝒫 𝑋)
122111, 121syl 17 . . . . 5 (πœ‘ β†’ 𝑋 ∈ 𝒫 𝑋)
123 neibastop1.2 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:π‘‹βŸΆ(𝒫 𝒫 𝑋 βˆ– {βˆ…}))
124123ffvelcdmda 7086 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}))
125 eldifi 4126 . . . . . . . . 9 ((πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}) β†’ (πΉβ€˜π‘₯) ∈ 𝒫 𝒫 𝑋)
126 elpwi 4609 . . . . . . . . 9 ((πΉβ€˜π‘₯) ∈ 𝒫 𝒫 𝑋 β†’ (πΉβ€˜π‘₯) βŠ† 𝒫 𝑋)
127124, 125, 1263syl 18 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) βŠ† 𝒫 𝑋)
128 df-ss 3965 . . . . . . . 8 ((πΉβ€˜π‘₯) βŠ† 𝒫 𝑋 ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) = (πΉβ€˜π‘₯))
129127, 128sylib 217 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) = (πΉβ€˜π‘₯))
130 eldifsni 4793 . . . . . . . 8 ((πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}) β†’ (πΉβ€˜π‘₯) β‰  βˆ…)
131124, 130syl 17 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) β‰  βˆ…)
132129, 131eqnetrd 3008 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
133132ralrimiva 3146 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
134 pweq 4616 . . . . . . . . 9 (π‘œ = 𝑋 β†’ 𝒫 π‘œ = 𝒫 𝑋)
135134ineq2d 4212 . . . . . . . 8 (π‘œ = 𝑋 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋))
136135neeq1d 3000 . . . . . . 7 (π‘œ = 𝑋 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
137136raleqbi1dv 3333 . . . . . 6 (π‘œ = 𝑋 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
138137, 2elrab2 3686 . . . . 5 (𝑋 ∈ 𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
139122, 133, 138sylanbrc 583 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝐽)
140 elssuni 4941 . . . 4 (𝑋 ∈ 𝐽 β†’ 𝑋 βŠ† βˆͺ 𝐽)
141139, 140syl 17 . . 3 (πœ‘ β†’ 𝑋 βŠ† βˆͺ 𝐽)
142141, 114eqssd 3999 . 2 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
143 istopon 22413 . 2 (𝐽 ∈ (TopOnβ€˜π‘‹) ↔ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝐽))
144120, 142, 143sylanbrc 583 1 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– cdif 3945   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908  βŸΆwf 6539  β€˜cfv 6543  Topctop 22394  TopOnctopon 22411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-top 22395  df-topon 22412
This theorem is referenced by:  neibastop2  35241  neibastop3  35242
  Copyright terms: Public domain W3C validator