Mathbox for ML < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  topdifinffinlem Structured version   Visualization version   GIF version

Theorem topdifinffinlem 34783
 Description: This is the core of the proof of topdifinffin 34784, 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 1915 . . . . 5 𝑢 ¬ 𝐴 ∈ Fin
2 nfab1 2957 . . . . 5 𝑢{𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
3 nfcv 2955 . . . . 5 𝑢𝑇
4 abid 2780 . . . . . . . . . . 11 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦𝐴 𝑢 = {𝑦})
5 df-rex 3112 . . . . . . . . . . 11 (∃𝑦𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
64, 5bitri 278 . . . . . . . . . 10 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
7 eqid 2798 . . . . . . . . . . . . . . 15 {𝑦} = {𝑦}
8 snex 5298 . . . . . . . . . . . . . . . . . 18 {𝑦} ∈ V
9 snelpwi 5303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
10 eleq1 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
119, 10syl5ibr 249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = {𝑦} → (𝑦𝐴𝑥 ∈ 𝒫 𝐴))
1211imdistani 572 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
1312anim2i 619 . . . . . . . . . . . . . . . . . . . . . . . 24 ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14133impb 1112 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15 3anass 1092 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
1614, 15sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17 snfi 8580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑦} ∈ Fin
18 eleq1 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
1917, 18mpbiri 261 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20 difinf 8775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴𝑥) ∈ Fin)
2119, 20sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴𝑥) ∈ Fin)
2221orcd 870 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
2322anim2i 619 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2423ancoms 462 . . . . . . . . . . . . . . . . . . . . . . 23 (((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
25243impa 1107 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2616, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27 topdifinf.t . . . . . . . . . . . . . . . . . . . . . 22 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
2827rabeq2i 3435 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2926, 28sylibr 237 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → 𝑥𝑇)
30 eleq1 2877 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = {𝑦} → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
31303ad2ant2 1131 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
3229, 31mpbid 235 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
3332sbcth 3735 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇))
348, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
35 sbcimg 3767 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
368, 35ax-mp 5 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
3734, 36mpbi 233 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38 sbc3an 3785 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
39 sbcg 3793 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
408, 39ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41403anbi1i 1154 . . . . . . . . . . . . . . . . . 18 (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
42 eqsbc3 3765 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
438, 42ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44433anbi2i 1155 . . . . . . . . . . . . . . . . . 18 ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
4538, 41, 443bitri 300 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
46 sbcg 3793 . . . . . . . . . . . . . . . . . . 19 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴))
478, 46ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴)
48473anbi3i 1156 . . . . . . . . . . . . . . . . 17 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
4945, 48bitri 278 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
50 sbcg 3793 . . . . . . . . . . . . . . . . 17 ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
518, 50ax-mp 5 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
5237, 49, 513imtr3i 294 . . . . . . . . . . . . . . 15 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
537, 52mp3an2 1446 . . . . . . . . . . . . . 14 ((¬ 𝐴 ∈ Fin ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
5453ex 416 . . . . . . . . . . . . 13 𝐴 ∈ Fin → (𝑦𝐴 → {𝑦} ∈ 𝑇))
5554pm4.71d 565 . . . . . . . . . . . 12 𝐴 ∈ Fin → (𝑦𝐴 ↔ (𝑦𝐴 ∧ {𝑦} ∈ 𝑇)))
5655anbi1d 632 . . . . . . . . . . 11 𝐴 ∈ Fin → ((𝑦𝐴𝑢 = {𝑦}) ↔ ((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
5756exbidv 1922 . . . . . . . . . 10 𝐴 ∈ Fin → (∃𝑦(𝑦𝐴𝑢 = {𝑦}) ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
586, 57syl5bb 286 . . . . . . . . 9 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59 anass 472 . . . . . . . . . . 11 (((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
6059exbii 1849 . . . . . . . . . 10 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
61 exsimpr 1870 . . . . . . . . . 10 (∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6260, 61sylbi 220 . . . . . . . . 9 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6358, 62syl6bi 256 . . . . . . . 8 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦})))
64 ancom 464 . . . . . . . . . 10 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65 eleq1 2877 . . . . . . . . . . 11 (𝑢 = {𝑦} → (𝑢𝑇 ↔ {𝑦} ∈ 𝑇))
6665pm5.32i 578 . . . . . . . . . 10 ((𝑢 = {𝑦} ∧ 𝑢𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
6764, 66bitr4i 281 . . . . . . . . 9 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢𝑇))
6867exbii 1849 . . . . . . . 8 (∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇))
6963, 68syl6ib 254 . . . . . . 7 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇)))
70 exsimpr 1870 . . . . . . 7 (∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇) → ∃𝑦 𝑢𝑇)
7169, 70syl6 35 . . . . . 6 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢𝑇))
72 ax5e 1913 . . . . . 6 (∃𝑦 𝑢𝑇𝑢𝑇)
7371, 72syl6 35 . . . . 5 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → 𝑢𝑇))
741, 2, 3, 73ssrd 3920 . . . 4 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75 eqid 2798 . . . . 5 {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
7675dissneq 34777 . . . 4 (({𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
7774, 76sylan 583 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78 nfielex 8734 . . . . 5 𝐴 ∈ Fin → ∃𝑦 𝑦𝐴)
7978adantr 484 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦𝐴)
80 difss 4059 . . . . . . 7 (𝐴 ∖ {𝑦}) ⊆ 𝐴
81 elfvex 6679 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82 difexg 5196 . . . . . . . 8 (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83 elpwg 4500 . . . . . . . 8 ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8481, 82, 833syl 18 . . . . . . 7 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8580, 84mpbiri 261 . . . . . 6 (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
8685adantl 485 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
87 difinf 8775 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
8817, 87mpan2 690 . . . . . . . . . . 11 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89 0fin 8733 . . . . . . . . . . . 12 ∅ ∈ Fin
90 eleq1 2877 . . . . . . . . . . . 12 ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
9189, 90mpbiri 261 . . . . . . . . . . 11 ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
9288, 91nsyl 142 . . . . . . . . . 10 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
9392ad2antrl 727 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94 vsnid 4562 . . . . . . . . . . . . . 14 𝑦 ∈ {𝑦}
95 inelcm 4372 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
9694, 95mpan2 690 . . . . . . . . . . . . 13 (𝑦𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97 disj4 4366 . . . . . . . . . . . . . 14 ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
9897necon2abii 3037 . . . . . . . . . . . . 13 ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
9996, 98sylibr 237 . . . . . . . . . . . 12 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
10099pssned 4026 . . . . . . . . . . 11 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101100adantr 484 . . . . . . . . . 10 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102101neneqd 2992 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
10393, 102jca 515 . . . . . . . 8 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104 pm4.56 986 . . . . . . . 8 ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105103, 104sylib 221 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
106 difeq2 4044 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
107106eleq1d 2874 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
108107notbid 321 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109 eqeq1 2802 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
110 eqeq1 2802 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
111109, 110orbi12d 916 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
112108, 111orbi12d 916 . . . . . . . . . . 11 (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
113112, 27elrab2 3631 . . . . . . . . . 10 ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
11485biantrurd 536 . . . . . . . . . 10 (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
115113, 114bitr4id 293 . . . . . . . . 9 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116 dfin4 4194 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117 inss2 4156 . . . . . . . . . . . 12 (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118 ssfi 8725 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
11917, 117, 118mp2an 691 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) ∈ Fin
120116, 119eqeltrri 2887 . . . . . . . . . 10 (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121 biortn 935 . . . . . . . . . 10 ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122120, 121ax-mp 5 . . . . . . . . 9 (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123115, 122bitr4di 292 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124123ad2antll 728 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125105, 124mtbird 328 . . . . . 6 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126125expcom 417 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127 nelneq2 2915 . . . . . 6 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128 eqcom 2805 . . . . . 6 (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129127, 128sylnibr 332 . . . . 5 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
13086, 126, 129syl6an 683 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ 𝑇 = 𝒫 𝐴))
13179, 130exellimddv 34781 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
13277, 131pm2.65da 816 . 2 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133132con4i 114 1 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∃wrex 3107  {crab 3110  Vcvv 3441  [wsbc 3720   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881   ⊊ wpss 3882  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ‘cfv 6325  Fincfn 8495  TopOnctopon 21525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-en 8496  df-fin 8499  df-topgen 16712  df-top 21509  df-topon 21526 This theorem is referenced by:  topdifinffin  34784
 Copyright terms: Public domain W3C validator