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 35244
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 486 . . . . . . . . 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 7729 . . . . . . . 8 βˆͺ 𝑦 ∈ V
98elpw 4607 . . . . . . 7 (βˆͺ 𝑦 ∈ 𝒫 𝑋 ↔ βˆͺ 𝑦 βŠ† 𝑋)
107, 9sylibr 233 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4913 . . . . . . . 8 (π‘₯ ∈ βˆͺ 𝑦 ↔ βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧)
12 elssuni 4942 . . . . . . . . . . . . 13 (𝑧 ∈ 𝑦 β†’ 𝑧 βŠ† βˆͺ 𝑦)
1312ad2antrl 727 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 βŠ† βˆͺ 𝑦)
1413sspwd 4616 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦)
15 sslin 4235 . . . . . . . . . . 11 (𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
1614, 15syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
171sselda 3983 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐽)
1817adantrr 716 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐽)
19 pweq 4617 . . . . . . . . . . . . . . . . 17 (π‘œ = 𝑧 β†’ 𝒫 π‘œ = 𝒫 𝑧)
2019ineq2d 4213 . . . . . . . . . . . . . . . 16 (π‘œ = 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
2120neeq1d 3001 . . . . . . . . . . . . . . 15 (π‘œ = 𝑧 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2221raleqbi1dv 3334 . . . . . . . . . . . . . 14 (π‘œ = 𝑧 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2322, 2elrab2 3687 . . . . . . . . . . . . 13 (𝑧 ∈ 𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2423simprbi 498 . . . . . . . . . . . 12 (𝑧 ∈ 𝐽 β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
2518, 24syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
26 simprr 772 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ π‘₯ ∈ 𝑧)
27 rsp 3245 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ (π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2825, 26, 27sylc 65 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
29 ssn0 4401 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3016, 28, 29syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3130rexlimdvaa 3157 . . . . . . . 8 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3211, 31biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (π‘₯ ∈ βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3332ralrimiv 3146 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
34 pweq 4617 . . . . . . . . . 10 (π‘œ = βˆͺ 𝑦 β†’ 𝒫 π‘œ = 𝒫 βˆͺ 𝑦)
3534ineq2d 4213 . . . . . . . . 9 (π‘œ = βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
3635neeq1d 3001 . . . . . . . 8 (π‘œ = βˆͺ 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3736raleqbi1dv 3334 . . . . . . 7 (π‘œ = βˆͺ 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3837, 2elrab2 3687 . . . . . 6 (βˆͺ 𝑦 ∈ 𝐽 ↔ (βˆͺ 𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3910, 33, 38sylanbrc 584 . . . . 5 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝐽)
4039ex 414 . . . 4 (πœ‘ β†’ (𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
4140alrimiv 1931 . . 3 (πœ‘ β†’ βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
42 pweq 4617 . . . . . . . . . . 11 (π‘œ = 𝑦 β†’ 𝒫 π‘œ = 𝒫 𝑦)
4342ineq2d 4213 . . . . . . . . . 10 (π‘œ = 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
4443neeq1d 3001 . . . . . . . . 9 (π‘œ = 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4544raleqbi1dv 3334 . . . . . . . 8 (π‘œ = 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4645, 2elrab2 3687 . . . . . . 7 (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4746, 23anbi12i 628 . . . . . 6 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
48 an4 655 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
4947, 48bitri 275 . . . . 5 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
50 inss1 4229 . . . . . . . . . 10 (𝑦 ∩ 𝑧) βŠ† 𝑦
51 elpwi 4610 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋 β†’ 𝑦 βŠ† 𝑋)
5250, 51sstrid 3994 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5352ad2antrl 727 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5453adantrr 716 . . . . . . 7 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
55 vex 3479 . . . . . . . . 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 614 . . . . . . . . 9 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
65 r19.26 3112 . . . . . . . . 9 (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
6664, 65sylibr 233 . . . . . . . 8 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
67 n0 4347 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
68 n0 4347 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… ↔ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
6967, 68anbi12i 628 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
70 exdistrv 1960 . . . . . . . . . . 11 (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
71 inss2 4230 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) βŠ† 𝒫 𝑦
72 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
7371, 72sselid 3981 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ 𝒫 𝑦)
7473elpwid 4612 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 βŠ† 𝑦)
75 inss2 4230 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 𝑧
76 simprr 772 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
7775, 76sselid 3981 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ 𝒫 𝑧)
7877elpwid 4612 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 βŠ† 𝑧)
79 ss2in 4237 . . . . . . . . . . . . . . . . 17 ((𝑣 βŠ† 𝑦 ∧ 𝑀 βŠ† 𝑧) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8074, 78, 79syl2anc 585 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8180sspwd 4616 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧))
82 sslin 4235 . . . . . . . . . . . . . . 15 (𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
8381, 82syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
84 simplll 774 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ πœ‘)
8553ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
86 simplr 768 . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
94 ssn0 4401 . . . . . . . . . . . . . 14 ((((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9583, 93, 94syl2anc 585 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9695ex 414 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9796exlimdvv 1938 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9870, 97biimtrrid 242 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9969, 98biimtrid 241 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10099ralimdva 3168 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10166, 100syl5 34 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
102101impr 456 . . . . . 6 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
103 pweq 4617 . . . . . . . . . 10 (π‘œ = (𝑦 ∩ 𝑧) β†’ 𝒫 π‘œ = 𝒫 (𝑦 ∩ 𝑧))
104103ineq2d 4213 . . . . . . . . 9 (π‘œ = (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
105104neeq1d 3001 . . . . . . . 8 (π‘œ = (𝑦 ∩ 𝑧) β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
106105raleqbi1dv 3334 . . . . . . 7 (π‘œ = (𝑦 ∩ 𝑧) β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
107106, 2elrab2 3687 . . . . . 6 ((𝑦 ∩ 𝑧) ∈ 𝐽 ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10858, 102, 107sylanbrc 584 . . . . 5 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
10949, 108sylan2b 595 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽)) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
110109ralrimivva 3201 . . 3 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)
111 neibastop1.1 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ 𝑉)
112 sspwuni 5104 . . . . . . . 8 (𝐽 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝐽 βŠ† 𝑋)
1134, 112mpbi 229 . . . . . . 7 βˆͺ 𝐽 βŠ† 𝑋
114113a1i 11 . . . . . 6 (πœ‘ β†’ βˆͺ 𝐽 βŠ† 𝑋)
115111, 114ssexd 5325 . . . . 5 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
116 uniexb 7751 . . . . 5 (𝐽 ∈ V ↔ βˆͺ 𝐽 ∈ V)
117115, 116sylibr 233 . . . 4 (πœ‘ β†’ 𝐽 ∈ V)
118 istopg 22397 . . . 4 (𝐽 ∈ V β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
119117, 118syl 17 . . 3 (πœ‘ β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
12041, 110, 119mpbir2and 712 . 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 3009 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
133132ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
134 pweq 4617 . . . . . . . . 9 (π‘œ = 𝑋 β†’ 𝒫 π‘œ = 𝒫 𝑋)
135134ineq2d 4213 . . . . . . . 8 (π‘œ = 𝑋 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋))
136135neeq1d 3001 . . . . . . 7 (π‘œ = 𝑋 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
137136raleqbi1dv 3334 . . . . . 6 (π‘œ = 𝑋 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
138137, 2elrab2 3687 . . . . 5 (𝑋 ∈ 𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
139122, 133, 138sylanbrc 584 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝐽)
140 elssuni 4942 . . . 4 (𝑋 ∈ 𝐽 β†’ 𝑋 βŠ† βˆͺ 𝐽)
141139, 140syl 17 . . 3 (πœ‘ β†’ 𝑋 βŠ† βˆͺ 𝐽)
142141, 114eqssd 4000 . 2 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
143 istopon 22414 . 2 (𝐽 ∈ (TopOnβ€˜π‘‹) ↔ (𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝐽))
144120, 142, 143sylanbrc 584 1 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βŸΆwf 6540  β€˜cfv 6544  Topctop 22395  TopOnctopon 22412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  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 22396  df-topon 22413
This theorem is referenced by:  neibastop2  35246  neibastop3  35247
  Copyright terms: Public domain W3C validator