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 34884
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 4041 . . . . . . . . . 10 {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…} βŠ† 𝒫 𝑋
42, 3eqsstri 3982 . . . . . . . . 9 𝐽 βŠ† 𝒫 𝑋
51, 4sstrdi 3960 . . . . . . . 8 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ 𝑦 βŠ† 𝒫 𝑋)
6 sspwuni 5064 . . . . . . . 8 (𝑦 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝑦 βŠ† 𝑋)
75, 6sylib 217 . . . . . . 7 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 βŠ† 𝑋)
8 vuniex 7680 . . . . . . . 8 βˆͺ 𝑦 ∈ V
98elpw 4568 . . . . . . 7 (βˆͺ 𝑦 ∈ 𝒫 𝑋 ↔ βˆͺ 𝑦 βŠ† 𝑋)
107, 9sylibr 233 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4873 . . . . . . . 8 (π‘₯ ∈ βˆͺ 𝑦 ↔ βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧)
12 elssuni 4902 . . . . . . . . . . . . 13 (𝑧 ∈ 𝑦 β†’ 𝑧 βŠ† βˆͺ 𝑦)
1312ad2antrl 727 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 βŠ† βˆͺ 𝑦)
1413sspwd 4577 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦)
15 sslin 4198 . . . . . . . . . . 11 (𝒫 𝑧 βŠ† 𝒫 βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
1614, 15syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
171sselda 3948 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐽)
1817adantrr 716 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐽)
19 pweq 4578 . . . . . . . . . . . . . . . . 17 (π‘œ = 𝑧 β†’ 𝒫 π‘œ = 𝒫 𝑧)
2019ineq2d 4176 . . . . . . . . . . . . . . . 16 (π‘œ = 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
2120neeq1d 3000 . . . . . . . . . . . . . . 15 (π‘œ = 𝑧 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2221raleqbi1dv 3306 . . . . . . . . . . . . . 14 (π‘œ = 𝑧 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2322, 2elrab2 3652 . . . . . . . . . . . . 13 (𝑧 ∈ 𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2423simprbi 498 . . . . . . . . . . . 12 (𝑧 ∈ 𝐽 β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
2518, 24syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
26 simprr 772 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ π‘₯ ∈ 𝑧)
27 rsp 3229 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ (π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
2825, 26, 27sylc 65 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
29 ssn0 4364 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3016, 28, 29syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 βŠ† 𝐽) ∧ (𝑧 ∈ 𝑦 ∧ π‘₯ ∈ 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
3130rexlimdvaa 3150 . . . . . . . 8 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (βˆƒπ‘§ ∈ 𝑦 π‘₯ ∈ 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3211, 31biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ (π‘₯ ∈ βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3332ralrimiv 3139 . . . . . 6 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…)
34 pweq 4578 . . . . . . . . . 10 (π‘œ = βˆͺ 𝑦 β†’ 𝒫 π‘œ = 𝒫 βˆͺ 𝑦)
3534ineq2d 4176 . . . . . . . . 9 (π‘œ = βˆͺ 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦))
3635neeq1d 3000 . . . . . . . 8 (π‘œ = βˆͺ 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3736raleqbi1dv 3306 . . . . . . 7 (π‘œ = βˆͺ 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3837, 2elrab2 3652 . . . . . 6 (βˆͺ 𝑦 ∈ 𝐽 ↔ (βˆͺ 𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ βˆͺ 𝑦((πΉβ€˜π‘₯) ∩ 𝒫 βˆͺ 𝑦) β‰  βˆ…))
3910, 33, 38sylanbrc 584 . . . . 5 ((πœ‘ ∧ 𝑦 βŠ† 𝐽) β†’ βˆͺ 𝑦 ∈ 𝐽)
4039ex 414 . . . 4 (πœ‘ β†’ (𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
4140alrimiv 1931 . . 3 (πœ‘ β†’ βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽))
42 pweq 4578 . . . . . . . . . . 11 (π‘œ = 𝑦 β†’ 𝒫 π‘œ = 𝒫 𝑦)
4342ineq2d 4176 . . . . . . . . . 10 (π‘œ = 𝑦 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
4443neeq1d 3000 . . . . . . . . 9 (π‘œ = 𝑦 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4544raleqbi1dv 3306 . . . . . . . 8 (π‘œ = 𝑦 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4645, 2elrab2 3652 . . . . . . 7 (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
4746, 23anbi12i 628 . . . . . 6 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
48 an4 655 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
4947, 48bitri 275 . . . . 5 ((𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)))
50 inss1 4192 . . . . . . . . . 10 (𝑦 ∩ 𝑧) βŠ† 𝑦
51 elpwi 4571 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋 β†’ 𝑦 βŠ† 𝑋)
5250, 51sstrid 3959 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5352ad2antrl 727 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5453adantrr 716 . . . . . . 7 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
55 vex 3451 . . . . . . . . 9 𝑦 ∈ V
5655inex1 5278 . . . . . . . 8 (𝑦 ∩ 𝑧) ∈ V
5756elpw 4568 . . . . . . 7 ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ↔ (𝑦 ∩ 𝑧) βŠ† 𝑋)
5854, 57sylibr 233 . . . . . 6 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) ∈ 𝒫 𝑋)
59 ssralv 4014 . . . . . . . . . . 11 ((𝑦 ∩ 𝑧) βŠ† 𝑦 β†’ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…))
6050, 59ax-mp 5 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ…)
61 inss2 4193 . . . . . . . . . . 11 (𝑦 ∩ 𝑧) βŠ† 𝑧
62 ssralv 4014 . . . . . . . . . . 11 ((𝑦 ∩ 𝑧) βŠ† 𝑧 β†’ (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
6361, 62ax-mp 5 . . . . . . . . . 10 (βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…)
6460, 63anim12i 614 . . . . . . . . 9 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
65 r19.26 3111 . . . . . . . . 9 (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
6664, 65sylibr 233 . . . . . . . 8 ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))
67 n0 4310 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
68 n0 4310 . . . . . . . . . . 11 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ… ↔ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
6967, 68anbi12i 628 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
70 exdistrv 1960 . . . . . . . . . . 11 (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) ↔ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)))
71 inss2 4193 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) βŠ† 𝒫 𝑦
72 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦))
7371, 72sselid 3946 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ 𝒫 𝑦)
7473elpwid 4573 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 βŠ† 𝑦)
75 inss2 4193 . . . . . . . . . . . . . . . . . . 19 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 𝑧
76 simprr 772 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
7775, 76sselid 3946 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ 𝒫 𝑧)
7877elpwid 4573 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 βŠ† 𝑧)
79 ss2in 4200 . . . . . . . . . . . . . . . . 17 ((𝑣 βŠ† 𝑦 ∧ 𝑀 βŠ† 𝑧) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8074, 78, 79syl2anc 585 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑣 ∩ 𝑀) βŠ† (𝑦 ∩ 𝑧))
8180sspwd 4577 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧))
82 sslin 4198 . . . . . . . . . . . . . . 15 (𝒫 (𝑣 ∩ 𝑀) βŠ† 𝒫 (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
8381, 82syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
84 simplll 774 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ πœ‘)
8553ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝑋)
86 simplr 768 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ π‘₯ ∈ (𝑦 ∩ 𝑧))
8785, 86sseldd 3949 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ π‘₯ ∈ 𝑋)
88 inss1 4192 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) βŠ† (πΉβ€˜π‘₯)
8988, 72sselid 3946 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑣 ∈ (πΉβ€˜π‘₯))
90 inss1 4192 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† (πΉβ€˜π‘₯)
9190, 76sselid 3946 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ 𝑀 ∈ (πΉβ€˜π‘₯))
92 neibastop1.3 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯) ∧ 𝑀 ∈ (πΉβ€˜π‘₯))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
9384, 87, 89, 91, 92syl13anc 1373 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
94 ssn0 4364 . . . . . . . . . . . . . 14 ((((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) βŠ† ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9583, 93, 94syl2anc 585 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) ∧ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
9695ex 414 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9796exlimdvv 1938 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ (βˆƒπ‘£βˆƒπ‘€(𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9870, 97biimtrrid 242 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) ∧ βˆƒπ‘€ 𝑀 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
9969, 98biimtrid 241 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) ∧ π‘₯ ∈ (𝑦 ∩ 𝑧)) β†’ ((((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10099ralimdva 3161 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ (βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)(((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10166, 100syl5 34 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋)) β†’ ((βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
102101impr 456 . . . . . 6 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…)
103 pweq 4578 . . . . . . . . . 10 (π‘œ = (𝑦 ∩ 𝑧) β†’ 𝒫 π‘œ = 𝒫 (𝑦 ∩ 𝑧))
104103ineq2d 4176 . . . . . . . . 9 (π‘œ = (𝑦 ∩ 𝑧) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)))
105104neeq1d 3000 . . . . . . . 8 (π‘œ = (𝑦 ∩ 𝑧) β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
106105raleqbi1dv 3306 . . . . . . 7 (π‘œ = (𝑦 ∩ 𝑧) β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
107106, 2elrab2 3652 . . . . . 6 ((𝑦 ∩ 𝑧) ∈ 𝐽 ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ (𝑦 ∩ 𝑧)((πΉβ€˜π‘₯) ∩ 𝒫 (𝑦 ∩ 𝑧)) β‰  βˆ…))
10858, 102, 107sylanbrc 584 . . . . 5 ((πœ‘ ∧ ((𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝒫 𝑋) ∧ (βˆ€π‘₯ ∈ 𝑦 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑦) β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑧 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) β‰  βˆ…))) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
10949, 108sylan2b 595 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝐽)) β†’ (𝑦 ∩ 𝑧) ∈ 𝐽)
110109ralrimivva 3194 . . 3 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)
111 neibastop1.1 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ 𝑉)
112 sspwuni 5064 . . . . . . . 8 (𝐽 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝐽 βŠ† 𝑋)
1134, 112mpbi 229 . . . . . . 7 βˆͺ 𝐽 βŠ† 𝑋
114113a1i 11 . . . . . 6 (πœ‘ β†’ βˆͺ 𝐽 βŠ† 𝑋)
115111, 114ssexd 5285 . . . . 5 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
116 uniexb 7702 . . . . 5 (𝐽 ∈ V ↔ βˆͺ 𝐽 ∈ V)
117115, 116sylibr 233 . . . 4 (πœ‘ β†’ 𝐽 ∈ V)
118 istopg 22267 . . . 4 (𝐽 ∈ V β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
119117, 118syl 17 . . 3 (πœ‘ β†’ (𝐽 ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† 𝐽 β†’ βˆͺ 𝑦 ∈ 𝐽) ∧ βˆ€π‘¦ ∈ 𝐽 βˆ€π‘§ ∈ 𝐽 (𝑦 ∩ 𝑧) ∈ 𝐽)))
12041, 110, 119mpbir2and 712 . 2 (πœ‘ β†’ 𝐽 ∈ Top)
121 pwidg 4584 . . . . . 6 (𝑋 ∈ 𝑉 β†’ 𝑋 ∈ 𝒫 𝑋)
122111, 121syl 17 . . . . 5 (πœ‘ β†’ 𝑋 ∈ 𝒫 𝑋)
123 neibastop1.2 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:π‘‹βŸΆ(𝒫 𝒫 𝑋 βˆ– {βˆ…}))
124123ffvelcdmda 7039 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}))
125 eldifi 4090 . . . . . . . . 9 ((πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}) β†’ (πΉβ€˜π‘₯) ∈ 𝒫 𝒫 𝑋)
126 elpwi 4571 . . . . . . . . 9 ((πΉβ€˜π‘₯) ∈ 𝒫 𝒫 𝑋 β†’ (πΉβ€˜π‘₯) βŠ† 𝒫 𝑋)
127124, 125, 1263syl 18 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) βŠ† 𝒫 𝑋)
128 df-ss 3931 . . . . . . . 8 ((πΉβ€˜π‘₯) βŠ† 𝒫 𝑋 ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) = (πΉβ€˜π‘₯))
129127, 128sylib 217 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) = (πΉβ€˜π‘₯))
130 eldifsni 4754 . . . . . . . 8 ((πΉβ€˜π‘₯) ∈ (𝒫 𝒫 𝑋 βˆ– {βˆ…}) β†’ (πΉβ€˜π‘₯) β‰  βˆ…)
131124, 130syl 17 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (πΉβ€˜π‘₯) β‰  βˆ…)
132129, 131eqnetrd 3008 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
133132ralrimiva 3140 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…)
134 pweq 4578 . . . . . . . . 9 (π‘œ = 𝑋 β†’ 𝒫 π‘œ = 𝒫 𝑋)
135134ineq2d 4176 . . . . . . . 8 (π‘œ = 𝑋 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋))
136135neeq1d 3000 . . . . . . 7 (π‘œ = 𝑋 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
137136raleqbi1dv 3306 . . . . . 6 (π‘œ = 𝑋 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
138137, 2elrab2 3652 . . . . 5 (𝑋 ∈ 𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑋) β‰  βˆ…))
139122, 133, 138sylanbrc 584 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝐽)
140 elssuni 4902 . . . 4 (𝑋 ∈ 𝐽 β†’ 𝑋 βŠ† βˆͺ 𝐽)
141139, 140syl 17 . . 3 (πœ‘ β†’ 𝑋 βŠ† βˆͺ 𝐽)
142141, 114eqssd 3965 . 2 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
143 istopon 22284 . 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 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3447   βˆ– cdif 3911   ∩ cin 3913   βŠ† wss 3914  βˆ…c0 4286  π’« cpw 4564  {csn 4590  βˆͺ cuni 4869  βŸΆwf 6496  β€˜cfv 6500  Topctop 22265  TopOnctopon 22282
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 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
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 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-top 22266  df-topon 22283
This theorem is referenced by:  neibastop2  34886  neibastop3  34887
  Copyright terms: Public domain W3C validator