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 33325
Description: This is the core of the proof of topdifinffin 33326, 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 1883 . . . . 5 𝑢 ¬ 𝐴 ∈ Fin
2 nfab1 2795 . . . . 5 𝑢{𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
3 nfcv 2793 . . . . 5 𝑢𝑇
4 abid 2639 . . . . . . . . . . 11 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦𝐴 𝑢 = {𝑦})
5 df-rex 2947 . . . . . . . . . . 11 (∃𝑦𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
64, 5bitri 264 . . . . . . . . . 10 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
7 eqid 2651 . . . . . . . . . . . . . . 15 {𝑦} = {𝑦}
8 snex 4938 . . . . . . . . . . . . . . . . . 18 {𝑦} ∈ V
9 snelpwi 4942 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
10 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
119, 10syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = {𝑦} → (𝑦𝐴𝑥 ∈ 𝒫 𝐴))
1211imdistani 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
1312anim2i 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14133impb 1279 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15 3anass 1059 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
1614, 15sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17 snfi 8079 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑦} ∈ Fin
18 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
1917, 18mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20 difinf 8271 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴𝑥) ∈ Fin)
2119, 20sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴𝑥) ∈ Fin)
2221orcd 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
2322anim2i 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2423ancoms 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
25243impa 1278 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2616, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27 topdifinf.t . . . . . . . . . . . . . . . . . . . . . 22 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
2827rabeq2i 3228 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2926, 28sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → 𝑥𝑇)
30 eleq1 2718 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = {𝑦} → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
31303ad2ant2 1103 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
3229, 31mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
3332sbcth 3483 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇))
348, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
35 sbcimg 3510 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
368, 35ax-mp 5 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
3734, 36mpbi 220 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38 sbc3an 3527 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
39 sbcg 3536 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
408, 39ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41403anbi1i 1272 . . . . . . . . . . . . . . . . . 18 (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
42 eqsbc3 3508 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
438, 42ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44433anbi2i 1273 . . . . . . . . . . . . . . . . . 18 ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
4538, 41, 443bitri 286 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
46 sbcg 3536 . . . . . . . . . . . . . . . . . . 19 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴))
478, 46ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴)
48473anbi3i 1274 . . . . . . . . . . . . . . . . 17 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
4945, 48bitri 264 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
50 sbcg 3536 . . . . . . . . . . . . . . . . 17 ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
518, 50ax-mp 5 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
5237, 49, 513imtr3i 280 . . . . . . . . . . . . . . 15 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
537, 52mp3an2 1452 . . . . . . . . . . . . . 14 ((¬ 𝐴 ∈ Fin ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
5453ex 449 . . . . . . . . . . . . 13 𝐴 ∈ Fin → (𝑦𝐴 → {𝑦} ∈ 𝑇))
5554pm4.71d 667 . . . . . . . . . . . 12 𝐴 ∈ Fin → (𝑦𝐴 ↔ (𝑦𝐴 ∧ {𝑦} ∈ 𝑇)))
5655anbi1d 741 . . . . . . . . . . 11 𝐴 ∈ Fin → ((𝑦𝐴𝑢 = {𝑦}) ↔ ((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
5756exbidv 1890 . . . . . . . . . 10 𝐴 ∈ Fin → (∃𝑦(𝑦𝐴𝑢 = {𝑦}) ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
586, 57syl5bb 272 . . . . . . . . 9 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59 anass 682 . . . . . . . . . . 11 (((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
6059exbii 1814 . . . . . . . . . 10 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
61 exsimpr 1836 . . . . . . . . . 10 (∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6260, 61sylbi 207 . . . . . . . . 9 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6358, 62syl6bi 243 . . . . . . . 8 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦})))
64 ancom 465 . . . . . . . . . 10 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65 eleq1 2718 . . . . . . . . . . 11 (𝑢 = {𝑦} → (𝑢𝑇 ↔ {𝑦} ∈ 𝑇))
6665pm5.32i 670 . . . . . . . . . 10 ((𝑢 = {𝑦} ∧ 𝑢𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
6764, 66bitr4i 267 . . . . . . . . 9 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢𝑇))
6867exbii 1814 . . . . . . . 8 (∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇))
6963, 68syl6ib 241 . . . . . . 7 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇)))
70 exsimpr 1836 . . . . . . 7 (∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇) → ∃𝑦 𝑢𝑇)
7169, 70syl6 35 . . . . . 6 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢𝑇))
72 ax5e 1881 . . . . . 6 (∃𝑦 𝑢𝑇𝑢𝑇)
7371, 72syl6 35 . . . . 5 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → 𝑢𝑇))
741, 2, 3, 73ssrd 3641 . . . 4 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75 eqid 2651 . . . . 5 {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
7675dissneq 33318 . . . 4 (({𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
7774, 76sylan 487 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78 nfielex 8230 . . . . 5 𝐴 ∈ Fin → ∃𝑦 𝑦𝐴)
7978adantr 480 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦𝐴)
80 difss 3770 . . . . . . 7 (𝐴 ∖ {𝑦}) ⊆ 𝐴
81 elfvex 6259 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82 difexg 4841 . . . . . . . 8 (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83 elpwg 4199 . . . . . . . 8 ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8481, 82, 833syl 18 . . . . . . 7 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8580, 84mpbiri 248 . . . . . 6 (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
8685adantl 481 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
87 difinf 8271 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
8817, 87mpan2 707 . . . . . . . . . . 11 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89 0fin 8229 . . . . . . . . . . . 12 ∅ ∈ Fin
90 eleq1 2718 . . . . . . . . . . . 12 ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
9189, 90mpbiri 248 . . . . . . . . . . 11 ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
9288, 91nsyl 135 . . . . . . . . . 10 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
9392ad2antrl 764 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94 vsnid 4242 . . . . . . . . . . . . . 14 𝑦 ∈ {𝑦}
95 inelcm 4065 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
9694, 95mpan2 707 . . . . . . . . . . . . 13 (𝑦𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97 disj4 4058 . . . . . . . . . . . . . 14 ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
9897necon2abii 2873 . . . . . . . . . . . . 13 ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
9996, 98sylibr 224 . . . . . . . . . . . 12 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
10099pssned 3738 . . . . . . . . . . 11 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101100adantr 480 . . . . . . . . . 10 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102101neneqd 2828 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
10393, 102jca 553 . . . . . . . 8 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104 pm4.56 515 . . . . . . . 8 ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105103, 104sylib 208 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
10685biantrurd 528 . . . . . . . . . 10 (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
107 difeq2 3755 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
108107eleq1d 2715 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109108notbid 307 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
110 eqeq1 2655 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
111 eqeq1 2655 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
112110, 111orbi12d 746 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
113109, 112orbi12d 746 . . . . . . . . . . 11 (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
114113, 27elrab2 3399 . . . . . . . . . 10 ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
115106, 114syl6rbbr 279 . . . . . . . . 9 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116 dfin4 3900 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117 inss2 3867 . . . . . . . . . . . 12 (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118 ssfi 8221 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
11917, 117, 118mp2an 708 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) ∈ Fin
120116, 119eqeltrri 2727 . . . . . . . . . 10 (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121 biortn 420 . . . . . . . . . 10 ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122120, 121ax-mp 5 . . . . . . . . 9 (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123115, 122syl6bbr 278 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124123ad2antll 765 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125105, 124mtbird 314 . . . . . 6 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126125expcom 450 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127 nelneq2 2755 . . . . . 6 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128 eqcom 2658 . . . . . 6 (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129127, 128sylnibr 318 . . . . 5 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
13086, 126, 129syl6an 567 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ 𝑇 = 𝒫 𝐴))
13179, 130exellimddv 33323 . . 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 382  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  {cab 2637  wne 2823  wrex 2942  {crab 2945  Vcvv 3231  [wsbc 3468  cdif 3604  cin 3606  wss 3607  wpss 3608  c0 3948  𝒫 cpw 4191  {csn 4210  cfv 5926  Fincfn 7997  TopOnctopon 20763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-fin 8001  df-topgen 16151  df-top 20747  df-topon 20764
This theorem is referenced by:  topdifinffin  33326
  Copyright terms: Public domain W3C validator