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 35548
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 484 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ 𝑦 βŠ† 𝐽)
2 neibastop1.4 . . . . . . . . . 10 𝐽 = {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…}
3 ssrab2 4078 . . . . . . . . . 10 {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…} βŠ† 𝒫 𝑋
42, 3eqsstri 4017 . . . . . . . . 9 𝐽 βŠ† 𝒫 𝑋
51, 4sstrdi 3995 . . . . . . . 8 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ 𝑦 βŠ† 𝒫 𝑋)
6 sspwuni 5104 . . . . . . . 8 (𝑦 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝑦 βŠ† 𝑋)
75, 6sylib 217 . . . . . . 7 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 βŠ† 𝑋)
8 vuniex 7732 . . . . . . . 8 βˆͺ 𝑦 ∈ V
98elpw 4607 . . . . . . 7 (βˆͺ 𝑦 ∈ 𝒫 𝑋 ↔ βˆͺ 𝑦 βŠ† 𝑋)
107, 9sylibr 233 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4913 . . . . . . . 8 (π‘₯ ∈ βˆͺ 𝑦 ↔ βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧)
12 elssuni 4942 . . . . . . . . . . . . 13 (𝑧 ∈ 𝑦 β†’ 𝑧 βŠ† βˆͺ 𝑦)
1312ad2antrl 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 βŠ† βˆͺ 𝑦)
1413sspwd 4616 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦)
15 sslin 4235 . . . . . . . . . . 11 (𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
1614, 15syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
171sselda 3983 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐽)
1817adantrr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐽)
19 pweq 4617 . . . . . . . . . . . . . . . . 17 (π‘œ = 𝑧 β†’ 𝒫 π‘œ = 𝒫 𝑧)
2019ineq2d 4213 . . . . . . . . . . . . . . . 16 (π‘œ = 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
2120neeq1d 2999 . . . . . . . . . . . . . . 15 (π‘œ = 𝑧 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2221raleqbi1dv 3332 . . . . . . . . . . . . . 14 (π‘œ = 𝑧 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2322, 2elrab2 3687 . . . . . . . . . . . . 13 (𝑧 ∈ 𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2423simprbi 496 . . . . . . . . . . . 12 (𝑧 ∈ 𝐽 β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
2518, 24syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
26 simprr 770 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ π‘₯ ∈ 𝑧)
27 rsp 3243 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ (π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2825, 26, 27sylc 65 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
29 ssn0 4401 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3016, 28, 29syl2anc 583 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3130rexlimdvaa 3155 . . . . . . . 8 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3211, 31biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (π‘₯ ∈ βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3332ralrimiv 3144 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
34 pweq 4617 . . . . . . . . . 10 (π‘œ = βˆͺ 𝑦 β†’ 𝒫 π‘œ = 𝒫 βˆͺ 𝑦)
3534ineq2d 4213 . . . . . . . . 9 (π‘œ = βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
3635neeq1d 2999 . . . . . . . 8 (π‘œ = βˆͺ 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3736raleqbi1dv 3332 . . . . . . 7 (π‘œ = βˆͺ 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3837, 2elrab2 3687 . . . . . 6 (βˆͺ 𝑦 ∈ 𝐽 ↔ (βˆͺ 𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3910, 33, 38sylanbrc 582 . . . . 5 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝐽)
4039ex 412 . . . 4 (πœ‘ β†’ (𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
4140alrimiv 1929 . . 3 (πœ‘ β†’ βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
42 pweq 4617 . . . . . . . . . . 11 (π‘œ = 𝑦 β†’ 𝒫 π‘œ = 𝒫 𝑦)
4342ineq2d 4213 . . . . . . . . . 10 (π‘œ = 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
4443neeq1d 2999 . . . . . . . . 9 (π‘œ = 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4544raleqbi1dv 3332 . . . . . . . 8 (π‘œ = 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4645, 2elrab2 3687 . . . . . . 7 (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4746, 23anbi12i 626 . . . . . 6 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
48 an4 653 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
4947, 48bitri 274 . . . . 5 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
50 inss1 4229 . . . . . . . . . 10 (𝑦 ∩ 𝑧) βŠ† 𝑦
51 elpwi 4610 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋 β†’ 𝑦 βŠ† 𝑋)
5250, 51sstrid 3994 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5352ad2antrl 725 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5453adantrr 714 . . . . . . 7 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
55 vex 3477 . . . . . . . . 9 𝑦 ∈ V
5655inex1 5318 . . . . . . . 8 (𝑦 ∩ 𝑧) ∈ V
5756elpw 4607 . . . . . . 7 ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ↔ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5854, 57sylibr 233 . . . . . 6 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) ∈ 𝒫 𝑋)
59 ssralv 4051 . . . . . . . . . . 11 ((𝑦 ∩ 𝑧) βŠ† 𝑦 β†’ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
6050, 59ax-mp 5 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…)
61 inss2 4230 . . . . . . . . . . 11 (𝑦 ∩ 𝑧) βŠ† 𝑧
62 ssralv 4051 . . . . . . . . . . 11 ((𝑦 ∩ 𝑧) βŠ† 𝑧 β†’ (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
6361, 62ax-mp 5 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
6460, 63anim12i 612 . . . . . . . . 9 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
65 r19.26 3110 . . . . . . . . 9 (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
6664, 65sylibr 233 . . . . . . . 8 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
67 n0 4347 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
68 n0 4347 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… ↔ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
6967, 68anbi12i 626 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
70 exdistrv 1958 . . . . . . . . . . 11 (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
71 inss2 4230 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) βŠ† 𝒫 𝑦
72 simprl 768 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
7371, 72sselid 3981 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ 𝒫 𝑦)
7473elpwid 4612 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 βŠ† 𝑦)
75 inss2 4230 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 𝑧
76 simprr 770 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
7775, 76sselid 3981 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ 𝒫 𝑧)
7877elpwid 4612 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 βŠ† 𝑧)
79 ss2in 4237 . . . . . . . . . . . . . . . . 17 ((𝑣 βŠ† 𝑦 ∧ 𝑀 βŠ† 𝑧) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8074, 78, 79syl2anc 583 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8180sspwd 4616 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧))
82 sslin 4235 . . . . . . . . . . . . . . 15 (𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
8381, 82syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
84 simplll 772 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ πœ‘)
8553ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
86 simplr 766 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ π‘₯ ∈ (𝑦 ∩ 𝑧))
8785, 86sseldd 3984 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ π‘₯ ∈ 𝑋)
88 inss1 4229 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) βŠ† (πΉβ€˜π‘₯)
8988, 72sselid 3981 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ (πΉβ€˜π‘₯))
90 inss1 4229 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† (πΉβ€˜π‘₯)
9190, 76sselid 3981 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ (πΉβ€˜π‘₯))
92 neibastop1.3 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯) ∧ 𝑀 ∈ (πΉβ€˜π‘₯))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
9384, 87, 89, 91, 92syl13anc 1371 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
94 ssn0 4401 . . . . . . . . . . . . . 14 ((((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9583, 93, 94syl2anc 583 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9695ex 412 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9796exlimdvv 1936 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9870, 97biimtrrid 242 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9969, 98biimtrid 241 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10099ralimdva 3166 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10166, 100syl5 34 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
102101impr 454 . . . . . 6 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
103 pweq 4617 . . . . . . . . . 10 (π‘œ = (𝑦 ∩ 𝑧) β†’ 𝒫 π‘œ = 𝒫 (𝑦 ∩ 𝑧))
104103ineq2d 4213 . . . . . . . . 9 (π‘œ = (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
105104neeq1d 2999 . . . . . . . 8 (π‘œ = (𝑦 ∩ 𝑧) β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
106105raleqbi1dv 3332 . . . . . . 7 (π‘œ = (𝑦 ∩ 𝑧) β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
107106, 2elrab2 3687 . . . . . 6 ((𝑦 ∩ 𝑧) ∈ 𝐽 ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10858, 102, 107sylanbrc 582 . . . . 5 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
10949, 108sylan2b 593 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽)) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
110109ralrimivva 3199 . . 3 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)
111 neibastop1.1 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ 𝑉)
112 sspwuni 5104 . . . . . . . 8 (𝐽 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝐽 βŠ† 𝑋)
1134, 112mpbi 229 . . . . . . 7 βˆͺ 𝐽 βŠ† 𝑋
114113a1i 11 . . . . . 6 (πœ‘ β†’ βˆͺ 𝐽 βŠ† 𝑋)
115111, 114ssexd 5325 . . . . 5 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
116 uniexb 7754 . . . . 5 (𝐽 ∈ V ↔ βˆͺ 𝐽 ∈ V)
117115, 116sylibr 233 . . . 4 (πœ‘ β†’ 𝐽 ∈ V)
118 istopg 22618 . . . 4 (𝐽 ∈ V β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
119117, 118syl 17 . . 3 (πœ‘ β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
12041, 110, 119mpbir2and 710 . 2 (πœ‘ β†’ 𝐽 ∈ Top)
121 pwidg 4623 . . . . . 6 (𝑋 ∈ 𝑉 β†’ 𝑋 ∈ 𝒫 𝑋)
122111, 121syl 17 . . . . 5 (πœ‘ β†’ 𝑋 ∈ 𝒫 𝑋)
123 neibastop1.2 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:π‘‹βŸΆ(𝒫 𝒫 𝑋 βˆ– {βˆ…}))
124123ffvelcdmda 7087 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}))
125 eldifi 4127 . . . . . . . . 9 ((πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}) β†’ (πΉβ€˜π‘₯) ∈ 𝒫 𝒫 𝑋)
126 elpwi 4610 . . . . . . . . 9 ((πΉβ€˜π‘₯) ∈ 𝒫 𝒫 𝑋 β†’ (πΉβ€˜π‘₯) βŠ† 𝒫 𝑋)
127124, 125, 1263syl 18 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) βŠ† 𝒫 𝑋)
128 df-ss 3966 . . . . . . . 8 ((πΉβ€˜π‘₯) βŠ† 𝒫 𝑋 ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) = (πΉβ€˜π‘₯))
129127, 128sylib 217 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) = (πΉβ€˜π‘₯))
130 eldifsni 4794 . . . . . . . 8 ((πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}) β†’ (πΉβ€˜π‘₯) β‰  βˆ…)
131124, 130syl 17 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) β‰  βˆ…)
132129, 131eqnetrd 3007 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
133132ralrimiva 3145 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
134 pweq 4617 . . . . . . . . 9 (π‘œ = 𝑋 β†’ 𝒫 π‘œ = 𝒫 𝑋)
135134ineq2d 4213 . . . . . . . 8 (π‘œ = 𝑋 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋))
136135neeq1d 2999 . . . . . . 7 (π‘œ = 𝑋 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
137136raleqbi1dv 3332 . . . . . 6 (π‘œ = 𝑋 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
138137, 2elrab2 3687 . . . . 5 (𝑋 ∈ 𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
139122, 133, 138sylanbrc 582 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝐽)
140 elssuni 4942 . . . 4 (𝑋 ∈ 𝐽 β†’ 𝑋 βŠ† βˆͺ 𝐽)
141139, 140syl 17 . . 3 (πœ‘ β†’ 𝑋 βŠ† βˆͺ 𝐽)
142141, 114eqssd 4000 . 2 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
143 istopon 22635 . 2 (𝐽 ∈ (TopOnβ€˜π‘‹) ↔ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝐽))
144120, 142, 143sylanbrc 582 1 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086  βˆ€wal 1538   = wceq 1540  βˆƒwex 1780   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  {crab 3431  Vcvv 3473   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βŸΆwf 6540  β€˜cfv 6544  Topctop 22616  TopOnctopon 22633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-top 22617  df-topon 22634
This theorem is referenced by:  neibastop2  35550  neibastop3  35551
  Copyright terms: Public domain W3C validator