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 32854
Description: This is the core of the proof of topdifinffin 32855, 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 1840 . . . . 5 𝑢 ¬ 𝐴 ∈ Fin
2 nfab1 2763 . . . . 5 𝑢{𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
3 nfcv 2761 . . . . 5 𝑢𝑇
4 abid 2609 . . . . . . . . . . 11 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦𝐴 𝑢 = {𝑦})
5 df-rex 2913 . . . . . . . . . . 11 (∃𝑦𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
64, 5bitri 264 . . . . . . . . . 10 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
7 eqid 2621 . . . . . . . . . . . . . . 15 {𝑦} = {𝑦}
8 snex 4874 . . . . . . . . . . . . . . . . . 18 {𝑦} ∈ V
9 snelpwi 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
10 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
119, 10syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = {𝑦} → (𝑦𝐴𝑥 ∈ 𝒫 𝐴))
1211imdistani 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
1312anim2i 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14133impb 1257 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15 3anass 1040 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
1614, 15sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17 snfi 7989 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑦} ∈ Fin
18 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
1917, 18mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20 difinf 8181 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴𝑥) ∈ Fin)
2119, 20sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴𝑥) ∈ Fin)
2221orcd 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
2322anim2i 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2423ancoms 469 . . . . . . . . . . . . . . . . . . . . . . 23 (((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
25243impa 1256 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2616, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27 topdifinf.t . . . . . . . . . . . . . . . . . . . . . 22 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
2827rabeq2i 3186 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2926, 28sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → 𝑥𝑇)
30 eleq1 2686 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = {𝑦} → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
31303ad2ant2 1081 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
3229, 31mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
3332sbcth 3436 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇))
348, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
35 sbcimg 3463 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
368, 35ax-mp 5 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
3734, 36mpbi 220 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38 sbc3an 3480 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
39 sbcg 3489 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
408, 39ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41403anbi1i 1251 . . . . . . . . . . . . . . . . . 18 (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
42 eqsbc3 3461 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
438, 42ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44433anbi2i 1252 . . . . . . . . . . . . . . . . . 18 ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
4538, 41, 443bitri 286 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
46 sbcg 3489 . . . . . . . . . . . . . . . . . . 19 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴))
478, 46ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴)
48473anbi3i 1253 . . . . . . . . . . . . . . . . 17 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
4945, 48bitri 264 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
50 sbcg 3489 . . . . . . . . . . . . . . . . 17 ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
518, 50ax-mp 5 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
5237, 49, 513imtr3i 280 . . . . . . . . . . . . . . 15 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
537, 52mp3an2 1409 . . . . . . . . . . . . . 14 ((¬ 𝐴 ∈ Fin ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
5453ex 450 . . . . . . . . . . . . 13 𝐴 ∈ Fin → (𝑦𝐴 → {𝑦} ∈ 𝑇))
5554pm4.71d 665 . . . . . . . . . . . 12 𝐴 ∈ Fin → (𝑦𝐴 ↔ (𝑦𝐴 ∧ {𝑦} ∈ 𝑇)))
5655anbi1d 740 . . . . . . . . . . 11 𝐴 ∈ Fin → ((𝑦𝐴𝑢 = {𝑦}) ↔ ((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
5756exbidv 1847 . . . . . . . . . 10 𝐴 ∈ Fin → (∃𝑦(𝑦𝐴𝑢 = {𝑦}) ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
586, 57syl5bb 272 . . . . . . . . 9 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59 anass 680 . . . . . . . . . . 11 (((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
6059exbii 1771 . . . . . . . . . 10 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
61 exsimpr 1793 . . . . . . . . . 10 (∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6260, 61sylbi 207 . . . . . . . . 9 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6358, 62syl6bi 243 . . . . . . . 8 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦})))
64 ancom 466 . . . . . . . . . 10 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65 eleq1 2686 . . . . . . . . . . 11 (𝑢 = {𝑦} → (𝑢𝑇 ↔ {𝑦} ∈ 𝑇))
6665pm5.32i 668 . . . . . . . . . 10 ((𝑢 = {𝑦} ∧ 𝑢𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
6764, 66bitr4i 267 . . . . . . . . 9 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢𝑇))
6867exbii 1771 . . . . . . . 8 (∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇))
6963, 68syl6ib 241 . . . . . . 7 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇)))
70 exsimpr 1793 . . . . . . 7 (∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇) → ∃𝑦 𝑢𝑇)
7169, 70syl6 35 . . . . . 6 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢𝑇))
72 ax5e 1838 . . . . . 6 (∃𝑦 𝑢𝑇𝑢𝑇)
7371, 72syl6 35 . . . . 5 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → 𝑢𝑇))
741, 2, 3, 73ssrd 3592 . . . 4 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75 eqid 2621 . . . . 5 {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
7675dissneq 32847 . . . 4 (({𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
7774, 76sylan 488 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78 nfielex 8140 . . . . 5 𝐴 ∈ Fin → ∃𝑦 𝑦𝐴)
7978adantr 481 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦𝐴)
80 difss 3720 . . . . . . 7 (𝐴 ∖ {𝑦}) ⊆ 𝐴
81 elfvex 6183 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82 difexg 4773 . . . . . . . 8 (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83 elpwg 4143 . . . . . . . 8 ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8481, 82, 833syl 18 . . . . . . 7 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8580, 84mpbiri 248 . . . . . 6 (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
8685adantl 482 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
87 difinf 8181 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
8817, 87mpan2 706 . . . . . . . . . . 11 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89 0fin 8139 . . . . . . . . . . . 12 ∅ ∈ Fin
90 eleq1 2686 . . . . . . . . . . . 12 ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
9189, 90mpbiri 248 . . . . . . . . . . 11 ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
9288, 91nsyl 135 . . . . . . . . . 10 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
9392ad2antrl 763 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94 vsnid 4185 . . . . . . . . . . . . . 14 𝑦 ∈ {𝑦}
95 inelcm 4009 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
9694, 95mpan2 706 . . . . . . . . . . . . 13 (𝑦𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97 disj4 4002 . . . . . . . . . . . . . 14 ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
9897necon2abii 2840 . . . . . . . . . . . . 13 ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
9996, 98sylibr 224 . . . . . . . . . . . 12 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
10099pssned 3688 . . . . . . . . . . 11 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101100adantr 481 . . . . . . . . . 10 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102101neneqd 2795 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
10393, 102jca 554 . . . . . . . 8 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104 pm4.56 516 . . . . . . . 8 ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105103, 104sylib 208 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
10685biantrurd 529 . . . . . . . . . 10 (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
107 difeq2 3705 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
108107eleq1d 2683 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109108notbid 308 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
110 eqeq1 2625 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
111 eqeq1 2625 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
112110, 111orbi12d 745 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
113109, 112orbi12d 745 . . . . . . . . . . 11 (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
114113, 27elrab2 3352 . . . . . . . . . 10 ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
115106, 114syl6rbbr 279 . . . . . . . . 9 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116 dfin4 3848 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117 inss2 3817 . . . . . . . . . . . 12 (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118 ssfi 8131 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
11917, 117, 118mp2an 707 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) ∈ Fin
120116, 119eqeltrri 2695 . . . . . . . . . 10 (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121 biortn 421 . . . . . . . . . 10 ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122120, 121ax-mp 5 . . . . . . . . 9 (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123115, 122syl6bbr 278 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124123ad2antll 764 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125105, 124mtbird 315 . . . . . 6 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126125expcom 451 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127 nelneq2 2723 . . . . . 6 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128 eqcom 2628 . . . . . 6 (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129127, 128sylnibr 319 . . . . 5 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
13086, 126, 129syl6an 567 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ 𝑇 = 𝒫 𝐴))
13179, 130exellimddv 32852 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
13277, 131pm2.65da 599 . 2 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133132con4i 113 1 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wne 2790  wrex 2908  {crab 2911  Vcvv 3189  [wsbc 3421  cdif 3556  cin 3558  wss 3559  wpss 3560  c0 3896  𝒫 cpw 4135  {csn 4153  cfv 5852  Fincfn 7906  TopOnctopon 20643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7907  df-fin 7910  df-topgen 16032  df-top 20627  df-topon 20644
This theorem is referenced by:  topdifinffin  32855
  Copyright terms: Public domain W3C validator