ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  epttop GIF version
Theorem epttop 13593
Description: The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
epttop ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ (TopOnβ€˜π΄))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝑃
Allowed substitution hint:   𝑉(π‘₯)
Proof of Theorem epttop
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab 3234 . . . . 5 (𝑦 βŠ† {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ↔ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)))
2 simprl 529 . . . . . . . . 9 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ 𝑦 βŠ† 𝒫 𝐴)
3 sspwuni 3972 . . . . . . . . 9 (𝑦 βŠ† 𝒫 𝐴 ↔ βˆͺ 𝑦 βŠ† 𝐴)
42, 3sylib 122 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ βˆͺ 𝑦 βŠ† 𝐴)
5 vuniex 4439 . . . . . . . . 9 βˆͺ 𝑦 ∈ V
65elpw 3582 . . . . . . . 8 (βˆͺ 𝑦 ∈ 𝒫 𝐴 ↔ βˆͺ 𝑦 βŠ† 𝐴)
74, 6sylibr 134 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ βˆͺ 𝑦 ∈ 𝒫 𝐴)
8 eluni2 3814 . . . . . . . . . 10 (𝑃 ∈ βˆͺ 𝑦 ↔ βˆƒπ‘₯ ∈ 𝑦 𝑃 ∈ π‘₯)
9 r19.29 2614 . . . . . . . . . . . . 13 ((βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ∧ βˆƒπ‘₯ ∈ 𝑦 𝑃 ∈ π‘₯) β†’ βˆƒπ‘₯ ∈ 𝑦 ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ∧ 𝑃 ∈ π‘₯))
10 simpr 110 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ 𝑦 ∧ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)) β†’ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))
1110impr 379 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑦 ∧ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ∧ 𝑃 ∈ π‘₯)) β†’ π‘₯ = 𝐴)
12 elssuni 3838 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝑦 β†’ π‘₯ βŠ† βˆͺ 𝑦)
1312adantr 276 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑦 ∧ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ∧ 𝑃 ∈ π‘₯)) β†’ π‘₯ βŠ† βˆͺ 𝑦)
1411, 13eqsstrrd 3193 . . . . . . . . . . . . . 14 ((π‘₯ ∈ 𝑦 ∧ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ∧ 𝑃 ∈ π‘₯)) β†’ 𝐴 βŠ† βˆͺ 𝑦)
1514rexlimiva 2589 . . . . . . . . . . . . 13 (βˆƒπ‘₯ ∈ 𝑦 ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ∧ 𝑃 ∈ π‘₯) β†’ 𝐴 βŠ† βˆͺ 𝑦)
169, 15syl 14 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ∧ βˆƒπ‘₯ ∈ 𝑦 𝑃 ∈ π‘₯) β†’ 𝐴 βŠ† βˆͺ 𝑦)
1716ex 115 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) β†’ (βˆƒπ‘₯ ∈ 𝑦 𝑃 ∈ π‘₯ β†’ 𝐴 βŠ† βˆͺ 𝑦))
1817ad2antll 491 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ (βˆƒπ‘₯ ∈ 𝑦 𝑃 ∈ π‘₯ β†’ 𝐴 βŠ† βˆͺ 𝑦))
198, 18biimtrid 152 . . . . . . . . 9 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ (𝑃 ∈ βˆͺ 𝑦 β†’ 𝐴 βŠ† βˆͺ 𝑦))
2019, 4jctild 316 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ (𝑃 ∈ βˆͺ 𝑦 β†’ (βˆͺ 𝑦 βŠ† 𝐴 ∧ 𝐴 βŠ† βˆͺ 𝑦)))
21 eqss 3171 . . . . . . . 8 (βˆͺ 𝑦 = 𝐴 ↔ (βˆͺ 𝑦 βŠ† 𝐴 ∧ 𝐴 βŠ† βˆͺ 𝑦))
2220, 21imbitrrdi 162 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ (𝑃 ∈ βˆͺ 𝑦 β†’ βˆͺ 𝑦 = 𝐴))
23 eleq2 2241 . . . . . . . . 9 (π‘₯ = βˆͺ 𝑦 β†’ (𝑃 ∈ π‘₯ ↔ 𝑃 ∈ βˆͺ 𝑦))
24 eqeq1 2184 . . . . . . . . 9 (π‘₯ = βˆͺ 𝑦 β†’ (π‘₯ = 𝐴 ↔ βˆͺ 𝑦 = 𝐴))
2523, 24imbi12d 234 . . . . . . . 8 (π‘₯ = βˆͺ 𝑦 β†’ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ↔ (𝑃 ∈ βˆͺ 𝑦 β†’ βˆͺ 𝑦 = 𝐴)))
2625elrab 2894 . . . . . . 7 (βˆͺ 𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ↔ (βˆͺ 𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ βˆͺ 𝑦 β†’ βˆͺ 𝑦 = 𝐴)))
277, 22, 26sylanbrc 417 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ (𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴))) β†’ βˆͺ 𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})
2827ex 115 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ ((𝑦 βŠ† 𝒫 𝐴 ∧ βˆ€π‘₯ ∈ 𝑦 (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)) β†’ βˆͺ 𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}))
291, 28biimtrid 152 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ (𝑦 βŠ† {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} β†’ βˆͺ 𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}))
3029alrimiv 1874 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ βˆ€π‘¦(𝑦 βŠ† {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} β†’ βˆͺ 𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}))
31 inss1 3356 . . . . . . . . 9 (𝑦 ∩ 𝑧) βŠ† 𝑦
32 simprll 537 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ 𝑦 ∈ 𝒫 𝐴)
3332elpwid 3587 . . . . . . . . 9 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ 𝑦 βŠ† 𝐴)
3431, 33sstrid 3167 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ (𝑦 ∩ 𝑧) βŠ† 𝐴)
35 vex 2741 . . . . . . . . . 10 𝑦 ∈ V
3635inex1 4138 . . . . . . . . 9 (𝑦 ∩ 𝑧) ∈ V
3736elpw 3582 . . . . . . . 8 ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ↔ (𝑦 ∩ 𝑧) βŠ† 𝐴)
3834, 37sylibr 134 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ (𝑦 ∩ 𝑧) ∈ 𝒫 𝐴)
39 elin 3319 . . . . . . . 8 (𝑃 ∈ (𝑦 ∩ 𝑧) ↔ (𝑃 ∈ 𝑦 ∧ 𝑃 ∈ 𝑧))
40 simprlr 538 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴))
41 simprrr 540 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴))
4240, 41anim12d 335 . . . . . . . . 9 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ ((𝑃 ∈ 𝑦 ∧ 𝑃 ∈ 𝑧) β†’ (𝑦 = 𝐴 ∧ 𝑧 = 𝐴)))
43 ineq12 3332 . . . . . . . . . 10 ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) β†’ (𝑦 ∩ 𝑧) = (𝐴 ∩ 𝐴))
44 inidm 3345 . . . . . . . . . 10 (𝐴 ∩ 𝐴) = 𝐴
4543, 44eqtrdi 2226 . . . . . . . . 9 ((𝑦 = 𝐴 ∧ 𝑧 = 𝐴) β†’ (𝑦 ∩ 𝑧) = 𝐴)
4642, 45syl6 33 . . . . . . . 8 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ ((𝑃 ∈ 𝑦 ∧ 𝑃 ∈ 𝑧) β†’ (𝑦 ∩ 𝑧) = 𝐴))
4739, 46biimtrid 152 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ (𝑃 ∈ (𝑦 ∩ 𝑧) β†’ (𝑦 ∩ 𝑧) = 𝐴))
4838, 47jca 306 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))) β†’ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ (𝑃 ∈ (𝑦 ∩ 𝑧) β†’ (𝑦 ∩ 𝑧) = 𝐴)))
4948ex 115 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ (((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴))) β†’ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ (𝑃 ∈ (𝑦 ∩ 𝑧) β†’ (𝑦 ∩ 𝑧) = 𝐴))))
50 eleq2 2241 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (𝑃 ∈ π‘₯ ↔ 𝑃 ∈ 𝑦))
51 eqeq1 2184 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (π‘₯ = 𝐴 ↔ 𝑦 = 𝐴))
5250, 51imbi12d 234 . . . . . . 7 (π‘₯ = 𝑦 β†’ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ↔ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)))
5352elrab 2894 . . . . . 6 (𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)))
54 eleq2 2241 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (𝑃 ∈ π‘₯ ↔ 𝑃 ∈ 𝑧))
55 eqeq1 2184 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (π‘₯ = 𝐴 ↔ 𝑧 = 𝐴))
5654, 55imbi12d 234 . . . . . . 7 (π‘₯ = 𝑧 β†’ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ↔ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))
5756elrab 2894 . . . . . 6 (𝑧 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴)))
5853, 57anbi12i 460 . . . . 5 ((𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∧ 𝑧 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}) ↔ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑦 β†’ 𝑦 = 𝐴)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝑧 β†’ 𝑧 = 𝐴))))
59 eleq2 2241 . . . . . . 7 (π‘₯ = (𝑦 ∩ 𝑧) β†’ (𝑃 ∈ π‘₯ ↔ 𝑃 ∈ (𝑦 ∩ 𝑧)))
60 eqeq1 2184 . . . . . . 7 (π‘₯ = (𝑦 ∩ 𝑧) β†’ (π‘₯ = 𝐴 ↔ (𝑦 ∩ 𝑧) = 𝐴))
6159, 60imbi12d 234 . . . . . 6 (π‘₯ = (𝑦 ∩ 𝑧) β†’ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ↔ (𝑃 ∈ (𝑦 ∩ 𝑧) β†’ (𝑦 ∩ 𝑧) = 𝐴)))
6261elrab 2894 . . . . 5 ((𝑦 ∩ 𝑧) ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ (𝑃 ∈ (𝑦 ∩ 𝑧) β†’ (𝑦 ∩ 𝑧) = 𝐴)))
6349, 58, 623imtr4g 205 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ ((𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∧ 𝑧 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}) β†’ (𝑦 ∩ 𝑧) ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}))
6463ralrimivv 2558 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}βˆ€π‘§ ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} (𝑦 ∩ 𝑧) ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})
65 pwexg 4181 . . . . . 6 (𝐴 ∈ 𝑉 β†’ 𝒫 𝐴 ∈ V)
6665adantr 276 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ 𝒫 𝐴 ∈ V)
67 rabexg 4147 . . . . 5 (𝒫 𝐴 ∈ V β†’ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ V)
6866, 67syl 14 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ V)
69 istopg 13502 . . . 4 ({π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ V β†’ ({π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} β†’ βˆͺ 𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}) ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}βˆ€π‘§ ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} (𝑦 ∩ 𝑧) ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})))
7068, 69syl 14 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ ({π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ Top ↔ (βˆ€π‘¦(𝑦 βŠ† {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} β†’ βˆͺ 𝑦 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}) ∧ βˆ€π‘¦ ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}βˆ€π‘§ ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} (𝑦 ∩ 𝑧) ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})))
7130, 64, 70mpbir2and 944 . 2 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ Top)
72 pwidg 3590 . . . . . 6 (𝐴 ∈ 𝑉 β†’ 𝐴 ∈ 𝒫 𝐴)
7372adantr 276 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ 𝐴 ∈ 𝒫 𝐴)
74 eqidd 2178 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ 𝐴 = 𝐴)
7574a1d 22 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ (𝑃 ∈ 𝐴 β†’ 𝐴 = 𝐴))
76 eleq2 2241 . . . . . . 7 (π‘₯ = 𝐴 β†’ (𝑃 ∈ π‘₯ ↔ 𝑃 ∈ 𝐴))
77 eqeq1 2184 . . . . . . 7 (π‘₯ = 𝐴 β†’ (π‘₯ = 𝐴 ↔ 𝐴 = 𝐴))
7876, 77imbi12d 234 . . . . . 6 (π‘₯ = 𝐴 β†’ ((𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴) ↔ (𝑃 ∈ 𝐴 β†’ 𝐴 = 𝐴)))
7978elrab 2894 . . . . 5 (𝐴 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ↔ (𝐴 ∈ 𝒫 𝐴 ∧ (𝑃 ∈ 𝐴 β†’ 𝐴 = 𝐴)))
8073, 75, 79sylanbrc 417 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ 𝐴 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})
81 elssuni 3838 . . . 4 (𝐴 ∈ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} β†’ 𝐴 βŠ† βˆͺ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})
8280, 81syl 14 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ 𝐴 βŠ† βˆͺ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})
83 ssrab2 3241 . . . . 5 {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} βŠ† 𝒫 𝐴
84 sspwuni 3972 . . . . 5 ({π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} βŠ† 𝒫 𝐴 ↔ βˆͺ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} βŠ† 𝐴)
8583, 84mpbi 145 . . . 4 βˆͺ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} βŠ† 𝐴
8685a1i 9 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ βˆͺ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} βŠ† 𝐴)
8782, 86eqssd 3173 . 2 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ 𝐴 = βˆͺ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)})
88 istopon 13516 . 2 ({π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ (TopOnβ€˜π΄) ↔ ({π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ Top ∧ 𝐴 = βˆͺ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)}))
8971, 87, 88sylanbrc 417 1 ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) β†’ {π‘₯ ∈ 𝒫 𝐴 ∣ (𝑃 ∈ π‘₯ β†’ π‘₯ = 𝐴)} ∈ (TopOnβ€˜π΄))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105  βˆ€wal 1351   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455  βˆƒwrex 2456  {crab 2459  Vcvv 2738   ∩ cin 3129   βŠ† wss 3130  π’« cpw 3576  βˆͺ cuni 3810  β€˜cfv 5217  Topctop 13500  TopOnctopon 13513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-sbc 2964  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-iota 5179  df-fun 5219  df-fv 5225  df-top 13501  df-topon 13514
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator