Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  topdifinffinlem Structured version   Visualization version   GIF version
Theorem topdifinffinlem 36532
Description: This is the core of the proof of topdifinffin 36533, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.)
Hypothesis
Ref Expression
topdifinf.t 𝑇 = {π‘₯ ∈ 𝒫 𝐴 ∣ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴))}
Assertion
Ref Expression
topdifinffinlem (𝑇 ∈ (TopOnβ€˜π΄) β†’ 𝐴 ∈ Fin)
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝑇
Proof of Theorem topdifinffinlem
Dummy variables 𝑒 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1916 . . . . 5 Ⅎ𝑒 Β¬ 𝐴 ∈ Fin
2 nfab1 2904 . . . . 5 Ⅎ𝑒{𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}}
3 nfcv 2902 . . . . 5 Ⅎ𝑒𝑇
4 abid 2712 . . . . . . . . . . 11 (𝑒 ∈ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} ↔ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦})
5 df-rex 3070 . . . . . . . . . . 11 (βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦} ↔ βˆƒπ‘¦(𝑦 ∈ 𝐴 ∧ 𝑒 = {𝑦}))
64, 5bitri 275 . . . . . . . . . 10 (𝑒 ∈ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} ↔ βˆƒπ‘¦(𝑦 ∈ 𝐴 ∧ 𝑒 = {𝑦}))
7 eqid 2731 . . . . . . . . . . . . . . 15 {𝑦} = {𝑦}
8 vsnex 5429 . . . . . . . . . . . . . . . . . 18 {𝑦} ∈ V
9 snelpwi 5443 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ 𝐴 β†’ {𝑦} ∈ 𝒫 𝐴)
10 eleq1 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘₯ = {𝑦} β†’ (π‘₯ ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
119, 10imbitrrid 245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ = {𝑦} β†’ (𝑦 ∈ 𝐴 β†’ π‘₯ ∈ 𝒫 𝐴))
1211imdistani 568 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ (π‘₯ = {𝑦} ∧ π‘₯ ∈ 𝒫 𝐴))
1312anim2i 616 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Β¬ 𝐴 ∈ Fin ∧ (π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴)) β†’ (Β¬ 𝐴 ∈ Fin ∧ (π‘₯ = {𝑦} ∧ π‘₯ ∈ 𝒫 𝐴)))
14133impb 1114 . . . . . . . . . . . . . . . . . . . . . . 23 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ (Β¬ 𝐴 ∈ Fin ∧ (π‘₯ = {𝑦} ∧ π‘₯ ∈ 𝒫 𝐴)))
15 3anass 1094 . . . . . . . . . . . . . . . . . . . . . . 23 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ π‘₯ ∈ 𝒫 𝐴) ↔ (Β¬ 𝐴 ∈ Fin ∧ (π‘₯ = {𝑦} ∧ π‘₯ ∈ 𝒫 𝐴)))
1614, 15sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ (Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ π‘₯ ∈ 𝒫 𝐴))
17 snfi 9048 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑦} ∈ Fin
18 eleq1 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ = {𝑦} β†’ (π‘₯ ∈ Fin ↔ {𝑦} ∈ Fin))
1917, 18mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘₯ = {𝑦} β†’ π‘₯ ∈ Fin)
20 difinf 9320 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ ∈ Fin) β†’ Β¬ (𝐴 βˆ– π‘₯) ∈ Fin)
2119, 20sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦}) β†’ Β¬ (𝐴 βˆ– π‘₯) ∈ Fin)
2221orcd 870 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦}) β†’ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴)))
2322anim2i 616 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘₯ ∈ 𝒫 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦})) β†’ (π‘₯ ∈ 𝒫 𝐴 ∧ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴))))
2423ancoms 458 . . . . . . . . . . . . . . . . . . . . . . 23 (((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦}) ∧ π‘₯ ∈ 𝒫 𝐴) β†’ (π‘₯ ∈ 𝒫 𝐴 ∧ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴))))
25243impa 1109 . . . . . . . . . . . . . . . . . . . . . 22 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ π‘₯ ∈ 𝒫 𝐴) β†’ (π‘₯ ∈ 𝒫 𝐴 ∧ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴))))
2616, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ (π‘₯ ∈ 𝒫 𝐴 ∧ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴))))
27 topdifinf.t . . . . . . . . . . . . . . . . . . . . . 22 𝑇 = {π‘₯ ∈ 𝒫 𝐴 ∣ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴))}
2827reqabi 3453 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ 𝑇 ↔ (π‘₯ ∈ 𝒫 𝐴 ∧ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴))))
2926, 28sylibr 233 . . . . . . . . . . . . . . . . . . . 20 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ π‘₯ ∈ 𝑇)
30 eleq1 2820 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = {𝑦} β†’ (π‘₯ ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
31303ad2ant2 1133 . . . . . . . . . . . . . . . . . . . 20 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ (π‘₯ ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
3229, 31mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ {𝑦} ∈ 𝑇)
3332sbcth 3792 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V β†’ [{𝑦} / π‘₯]((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ {𝑦} ∈ 𝑇))
348, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 [{𝑦} / π‘₯]((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ {𝑦} ∈ 𝑇)
35 sbcimg 3828 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V β†’ ([{𝑦} / π‘₯]((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ {𝑦} ∈ 𝑇) ↔ ([{𝑦} / π‘₯](Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ [{𝑦} / π‘₯]{𝑦} ∈ 𝑇)))
368, 35ax-mp 5 . . . . . . . . . . . . . . . . 17 ([{𝑦} / π‘₯]((Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ {𝑦} ∈ 𝑇) ↔ ([{𝑦} / π‘₯](Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ [{𝑦} / π‘₯]{𝑦} ∈ 𝑇))
3734, 36mpbi 229 . . . . . . . . . . . . . . . 16 ([{𝑦} / π‘₯](Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ [{𝑦} / π‘₯]{𝑦} ∈ 𝑇)
38 sbc3an 3847 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / π‘₯](Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ ([{𝑦} / π‘₯] Β¬ 𝐴 ∈ Fin ∧ [{𝑦} / π‘₯]π‘₯ = {𝑦} ∧ [{𝑦} / π‘₯]𝑦 ∈ 𝐴))
39 sbcg 3856 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V β†’ ([{𝑦} / π‘₯] Β¬ 𝐴 ∈ Fin ↔ Β¬ 𝐴 ∈ Fin))
408, 39ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / π‘₯] Β¬ 𝐴 ∈ Fin ↔ Β¬ 𝐴 ∈ Fin)
41403anbi1i 1156 . . . . . . . . . . . . . . . . . 18 (([{𝑦} / π‘₯] Β¬ 𝐴 ∈ Fin ∧ [{𝑦} / π‘₯]π‘₯ = {𝑦} ∧ [{𝑦} / π‘₯]𝑦 ∈ 𝐴) ↔ (Β¬ 𝐴 ∈ Fin ∧ [{𝑦} / π‘₯]π‘₯ = {𝑦} ∧ [{𝑦} / π‘₯]𝑦 ∈ 𝐴))
42 eqsbc1 3826 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V β†’ ([{𝑦} / π‘₯]π‘₯ = {𝑦} ↔ {𝑦} = {𝑦}))
438, 42ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / π‘₯]π‘₯ = {𝑦} ↔ {𝑦} = {𝑦})
44433anbi2i 1157 . . . . . . . . . . . . . . . . . 18 ((Β¬ 𝐴 ∈ Fin ∧ [{𝑦} / π‘₯]π‘₯ = {𝑦} ∧ [{𝑦} / π‘₯]𝑦 ∈ 𝐴) ↔ (Β¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / π‘₯]𝑦 ∈ 𝐴))
4538, 41, 443bitri 297 . . . . . . . . . . . . . . . . 17 ([{𝑦} / π‘₯](Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (Β¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / π‘₯]𝑦 ∈ 𝐴))
46 sbcg 3856 . . . . . . . . . . . . . . . . . . 19 ({𝑦} ∈ V β†’ ([{𝑦} / π‘₯]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
478, 46ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / π‘₯]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
48473anbi3i 1158 . . . . . . . . . . . . . . . . 17 ((Β¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / π‘₯]𝑦 ∈ 𝐴) ↔ (Β¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
4945, 48bitri 275 . . . . . . . . . . . . . . . 16 ([{𝑦} / π‘₯](Β¬ 𝐴 ∈ Fin ∧ π‘₯ = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (Β¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴))
50 sbcg 3856 . . . . . . . . . . . . . . . . 17 ({𝑦} ∈ V β†’ ([{𝑦} / π‘₯]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
518, 50ax-mp 5 . . . . . . . . . . . . . . . 16 ([{𝑦} / π‘₯]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
5237, 49, 513imtr3i 291 . . . . . . . . . . . . . . 15 ((Β¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴) β†’ {𝑦} ∈ 𝑇)
537, 52mp3an2 1448 . . . . . . . . . . . . . 14 ((Β¬ 𝐴 ∈ Fin ∧ 𝑦 ∈ 𝐴) β†’ {𝑦} ∈ 𝑇)
5453ex 412 . . . . . . . . . . . . 13 (Β¬ 𝐴 ∈ Fin β†’ (𝑦 ∈ 𝐴 β†’ {𝑦} ∈ 𝑇))
5554pm4.71d 561 . . . . . . . . . . . 12 (Β¬ 𝐴 ∈ Fin β†’ (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇)))
5655anbi1d 629 . . . . . . . . . . 11 (Β¬ 𝐴 ∈ Fin β†’ ((𝑦 ∈ 𝐴 ∧ 𝑒 = {𝑦}) ↔ ((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑒 = {𝑦})))
5756exbidv 1923 . . . . . . . . . 10 (Β¬ 𝐴 ∈ Fin β†’ (βˆƒπ‘¦(𝑦 ∈ 𝐴 ∧ 𝑒 = {𝑦}) ↔ βˆƒπ‘¦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑒 = {𝑦})))
586, 57bitrid 283 . . . . . . . . 9 (Β¬ 𝐴 ∈ Fin β†’ (𝑒 ∈ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} ↔ βˆƒπ‘¦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑒 = {𝑦})))
59 anass 468 . . . . . . . . . . 11 (((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑒 = {𝑦}) ↔ (𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦})))
6059exbii 1849 . . . . . . . . . 10 (βˆƒπ‘¦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑒 = {𝑦}) ↔ βˆƒπ‘¦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦})))
61 exsimpr 1871 . . . . . . . . . 10 (βˆƒπ‘¦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦})) β†’ βˆƒπ‘¦({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦}))
6260, 61sylbi 216 . . . . . . . . 9 (βˆƒπ‘¦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑒 = {𝑦}) β†’ βˆƒπ‘¦({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦}))
6358, 62syl6bi 253 . . . . . . . 8 (Β¬ 𝐴 ∈ Fin β†’ (𝑒 ∈ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} β†’ βˆƒπ‘¦({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦})))
64 ancom 460 . . . . . . . . . 10 (({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦}) ↔ (𝑒 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65 eleq1 2820 . . . . . . . . . . 11 (𝑒 = {𝑦} β†’ (𝑒 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
6665pm5.32i 574 . . . . . . . . . 10 ((𝑒 = {𝑦} ∧ 𝑒 ∈ 𝑇) ↔ (𝑒 = {𝑦} ∧ {𝑦} ∈ 𝑇))
6764, 66bitr4i 278 . . . . . . . . 9 (({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦}) ↔ (𝑒 = {𝑦} ∧ 𝑒 ∈ 𝑇))
6867exbii 1849 . . . . . . . 8 (βˆƒπ‘¦({𝑦} ∈ 𝑇 ∧ 𝑒 = {𝑦}) ↔ βˆƒπ‘¦(𝑒 = {𝑦} ∧ 𝑒 ∈ 𝑇))
6963, 68imbitrdi 250 . . . . . . 7 (Β¬ 𝐴 ∈ Fin β†’ (𝑒 ∈ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} β†’ βˆƒπ‘¦(𝑒 = {𝑦} ∧ 𝑒 ∈ 𝑇)))
70 exsimpr 1871 . . . . . . 7 (βˆƒπ‘¦(𝑒 = {𝑦} ∧ 𝑒 ∈ 𝑇) β†’ βˆƒπ‘¦ 𝑒 ∈ 𝑇)
7169, 70syl6 35 . . . . . 6 (Β¬ 𝐴 ∈ Fin β†’ (𝑒 ∈ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} β†’ βˆƒπ‘¦ 𝑒 ∈ 𝑇))
72 ax5e 1914 . . . . . 6 (βˆƒπ‘¦ 𝑒 ∈ 𝑇 β†’ 𝑒 ∈ 𝑇)
7371, 72syl6 35 . . . . 5 (Β¬ 𝐴 ∈ Fin β†’ (𝑒 ∈ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} β†’ 𝑒 ∈ 𝑇))
741, 2, 3, 73ssrd 3987 . . . 4 (Β¬ 𝐴 ∈ Fin β†’ {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} βŠ† 𝑇)
75 eqid 2731 . . . . 5 {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} = {𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}}
7675dissneq 36526 . . . 4 (({𝑒 ∣ βˆƒπ‘¦ ∈ 𝐴 𝑒 = {𝑦}} βŠ† 𝑇 ∧ 𝑇 ∈ (TopOnβ€˜π΄)) β†’ 𝑇 = 𝒫 𝐴)
7774, 76sylan 579 . . 3 ((Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄)) β†’ 𝑇 = 𝒫 𝐴)
78 nfielex 9277 . . . . 5 (Β¬ 𝐴 ∈ Fin β†’ βˆƒπ‘¦ 𝑦 ∈ 𝐴)
7978adantr 480 . . . 4 ((Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄)) β†’ βˆƒπ‘¦ 𝑦 ∈ 𝐴)
80 difss 4131 . . . . . . 7 (𝐴 βˆ– {𝑦}) βŠ† 𝐴
81 elfvex 6929 . . . . . . . 8 (𝑇 ∈ (TopOnβ€˜π΄) β†’ 𝐴 ∈ V)
82 difexg 5327 . . . . . . . 8 (𝐴 ∈ V β†’ (𝐴 βˆ– {𝑦}) ∈ V)
83 elpwg 4605 . . . . . . . 8 ((𝐴 βˆ– {𝑦}) ∈ V β†’ ((𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 βˆ– {𝑦}) βŠ† 𝐴))
8481, 82, 833syl 18 . . . . . . 7 (𝑇 ∈ (TopOnβ€˜π΄) β†’ ((𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 βˆ– {𝑦}) βŠ† 𝐴))
8580, 84mpbiri 258 . . . . . 6 (𝑇 ∈ (TopOnβ€˜π΄) β†’ (𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴)
8685adantl 481 . . . . 5 ((Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄)) β†’ (𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴)
87 difinf 9320 . . . . . . . . . . . 12 ((Β¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) β†’ Β¬ (𝐴 βˆ– {𝑦}) ∈ Fin)
8817, 87mpan2 688 . . . . . . . . . . 11 (Β¬ 𝐴 ∈ Fin β†’ Β¬ (𝐴 βˆ– {𝑦}) ∈ Fin)
89 0fin 9175 . . . . . . . . . . . 12 βˆ… ∈ Fin
90 eleq1 2820 . . . . . . . . . . . 12 ((𝐴 βˆ– {𝑦}) = βˆ… β†’ ((𝐴 βˆ– {𝑦}) ∈ Fin ↔ βˆ… ∈ Fin))
9189, 90mpbiri 258 . . . . . . . . . . 11 ((𝐴 βˆ– {𝑦}) = βˆ… β†’ (𝐴 βˆ– {𝑦}) ∈ Fin)
9288, 91nsyl 140 . . . . . . . . . 10 (Β¬ 𝐴 ∈ Fin β†’ Β¬ (𝐴 βˆ– {𝑦}) = βˆ…)
9392ad2antrl 725 . . . . . . . . 9 ((𝑦 ∈ 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄))) β†’ Β¬ (𝐴 βˆ– {𝑦}) = βˆ…)
94 vsnid 4665 . . . . . . . . . . . . . 14 𝑦 ∈ {𝑦}
95 inelcm 4464 . . . . . . . . . . . . . 14 ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦}) β†’ (𝐴 ∩ {𝑦}) β‰  βˆ…)
9694, 95mpan2 688 . . . . . . . . . . . . 13 (𝑦 ∈ 𝐴 β†’ (𝐴 ∩ {𝑦}) β‰  βˆ…)
97 disj4 4458 . . . . . . . . . . . . . 14 ((𝐴 ∩ {𝑦}) = βˆ… ↔ Β¬ (𝐴 βˆ– {𝑦}) ⊊ 𝐴)
9897necon2abii 2990 . . . . . . . . . . . . 13 ((𝐴 βˆ– {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) β‰  βˆ…)
9996, 98sylibr 233 . . . . . . . . . . . 12 (𝑦 ∈ 𝐴 β†’ (𝐴 βˆ– {𝑦}) ⊊ 𝐴)
10099pssned 4098 . . . . . . . . . . 11 (𝑦 ∈ 𝐴 β†’ (𝐴 βˆ– {𝑦}) β‰  𝐴)
101100adantr 480 . . . . . . . . . 10 ((𝑦 ∈ 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄))) β†’ (𝐴 βˆ– {𝑦}) β‰  𝐴)
102101neneqd 2944 . . . . . . . . 9 ((𝑦 ∈ 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄))) β†’ Β¬ (𝐴 βˆ– {𝑦}) = 𝐴)
10393, 102jca 511 . . . . . . . 8 ((𝑦 ∈ 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄))) β†’ (Β¬ (𝐴 βˆ– {𝑦}) = βˆ… ∧ Β¬ (𝐴 βˆ– {𝑦}) = 𝐴))
104 pm4.56 986 . . . . . . . 8 ((Β¬ (𝐴 βˆ– {𝑦}) = βˆ… ∧ Β¬ (𝐴 βˆ– {𝑦}) = 𝐴) ↔ Β¬ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴))
105103, 104sylib 217 . . . . . . 7 ((𝑦 ∈ 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄))) β†’ Β¬ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴))
106 difeq2 4116 . . . . . . . . . . . . . 14 (π‘₯ = (𝐴 βˆ– {𝑦}) β†’ (𝐴 βˆ– π‘₯) = (𝐴 βˆ– (𝐴 βˆ– {𝑦})))
107106eleq1d 2817 . . . . . . . . . . . . 13 (π‘₯ = (𝐴 βˆ– {𝑦}) β†’ ((𝐴 βˆ– π‘₯) ∈ Fin ↔ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin))
108107notbid 318 . . . . . . . . . . . 12 (π‘₯ = (𝐴 βˆ– {𝑦}) β†’ (Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ↔ Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin))
109 eqeq1 2735 . . . . . . . . . . . . 13 (π‘₯ = (𝐴 βˆ– {𝑦}) β†’ (π‘₯ = βˆ… ↔ (𝐴 βˆ– {𝑦}) = βˆ…))
110 eqeq1 2735 . . . . . . . . . . . . 13 (π‘₯ = (𝐴 βˆ– {𝑦}) β†’ (π‘₯ = 𝐴 ↔ (𝐴 βˆ– {𝑦}) = 𝐴))
111109, 110orbi12d 916 . . . . . . . . . . . 12 (π‘₯ = (𝐴 βˆ– {𝑦}) β†’ ((π‘₯ = βˆ… ∨ π‘₯ = 𝐴) ↔ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴)))
112108, 111orbi12d 916 . . . . . . . . . . 11 (π‘₯ = (𝐴 βˆ– {𝑦}) β†’ ((Β¬ (𝐴 βˆ– π‘₯) ∈ Fin ∨ (π‘₯ = βˆ… ∨ π‘₯ = 𝐴)) ↔ (Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin ∨ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴))))
113112, 27elrab2 3686 . . . . . . . . . 10 ((𝐴 βˆ– {𝑦}) ∈ 𝑇 ↔ ((𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴 ∧ (Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin ∨ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴))))
11485biantrurd 532 . . . . . . . . . 10 (𝑇 ∈ (TopOnβ€˜π΄) β†’ ((Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin ∨ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴)) ↔ ((𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴 ∧ (Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin ∨ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴)))))
115113, 114bitr4id 290 . . . . . . . . 9 (𝑇 ∈ (TopOnβ€˜π΄) β†’ ((𝐴 βˆ– {𝑦}) ∈ 𝑇 ↔ (Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin ∨ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴))))
116 dfin4 4267 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) = (𝐴 βˆ– (𝐴 βˆ– {𝑦}))
117 inss2 4229 . . . . . . . . . . . 12 (𝐴 ∩ {𝑦}) βŠ† {𝑦}
118 ssfi 9177 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) βŠ† {𝑦}) β†’ (𝐴 ∩ {𝑦}) ∈ Fin)
11917, 117, 118mp2an 689 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) ∈ Fin
120116, 119eqeltrri 2829 . . . . . . . . . 10 (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin
121 biortn 935 . . . . . . . . . 10 ((𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin β†’ (((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴) ↔ (Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin ∨ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴))))
122120, 121ax-mp 5 . . . . . . . . 9 (((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴) ↔ (Β¬ (𝐴 βˆ– (𝐴 βˆ– {𝑦})) ∈ Fin ∨ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴)))
123115, 122bitr4di 289 . . . . . . . 8 (𝑇 ∈ (TopOnβ€˜π΄) β†’ ((𝐴 βˆ– {𝑦}) ∈ 𝑇 ↔ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴)))
124123ad2antll 726 . . . . . . 7 ((𝑦 ∈ 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄))) β†’ ((𝐴 βˆ– {𝑦}) ∈ 𝑇 ↔ ((𝐴 βˆ– {𝑦}) = βˆ… ∨ (𝐴 βˆ– {𝑦}) = 𝐴)))
125105, 124mtbird 325 . . . . . 6 ((𝑦 ∈ 𝐴 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄))) β†’ Β¬ (𝐴 βˆ– {𝑦}) ∈ 𝑇)
126125expcom 413 . . . . 5 ((Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄)) β†’ (𝑦 ∈ 𝐴 β†’ Β¬ (𝐴 βˆ– {𝑦}) ∈ 𝑇))
127 nelneq2 2857 . . . . . 6 (((𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴 ∧ Β¬ (𝐴 βˆ– {𝑦}) ∈ 𝑇) β†’ Β¬ 𝒫 𝐴 = 𝑇)
128 eqcom 2738 . . . . . 6 (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129127, 128sylnibr 329 . . . . 5 (((𝐴 βˆ– {𝑦}) ∈ 𝒫 𝐴 ∧ Β¬ (𝐴 βˆ– {𝑦}) ∈ 𝑇) β†’ Β¬ 𝑇 = 𝒫 𝐴)
13086, 126, 129syl6an 681 . . . 4 ((Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄)) β†’ (𝑦 ∈ 𝐴 β†’ Β¬ 𝑇 = 𝒫 𝐴))
13179, 130exellimddv 36530 . . 3 ((Β¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOnβ€˜π΄)) β†’ Β¬ 𝑇 = 𝒫 𝐴)
13277, 131pm2.65da 814 . 2 (Β¬ 𝐴 ∈ Fin β†’ Β¬ 𝑇 ∈ (TopOnβ€˜π΄))
133132con4i 114 1 (𝑇 ∈ (TopOnβ€˜π΄) β†’ 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1086   = wceq 1540  βˆƒwex 1780   ∈ wcel 2105  {cab 2708   β‰  wne 2939  βˆƒwrex 3069  {crab 3431  Vcvv 3473  [wsbc 3777   βˆ– cdif 3945   ∩ cin 3947   βŠ† wss 3948   ⊊ wpss 3949  βˆ…c0 4322  π’« cpw 4602  {csn 4628  β€˜cfv 6543  Fincfn 8943  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 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  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-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  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-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7860  df-1o 8470  df-en 8944  df-fin 8947  df-topgen 17394  df-top 22617  df-topon 22634
This theorem is referenced by:  topdifinffin  36533
  Copyright terms: Public domain W3C validator