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 37330
Description: This is the core of the proof of topdifinffin 37331, 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 1912 . . . . 5 𝑢 ¬ 𝐴 ∈ Fin
2 nfab1 2905 . . . . 5 𝑢{𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
3 nfcv 2903 . . . . 5 𝑢𝑇
4 abid 2716 . . . . . . . . . . 11 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦𝐴 𝑢 = {𝑦})
5 df-rex 3069 . . . . . . . . . . 11 (∃𝑦𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
64, 5bitri 275 . . . . . . . . . 10 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
7 eqid 2735 . . . . . . . . . . . . . . 15 {𝑦} = {𝑦}
8 vsnex 5440 . . . . . . . . . . . . . . . . . 18 {𝑦} ∈ V
9 snelpwi 5454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
10 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
119, 10imbitrrid 246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = {𝑦} → (𝑦𝐴𝑥 ∈ 𝒫 𝐴))
1211imdistani 568 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
1312anim2i 617 . . . . . . . . . . . . . . . . . . . . . . . 24 ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14133impb 1114 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15 3anass 1094 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
1614, 15sylibr 234 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17 snfi 9082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑦} ∈ Fin
18 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
1917, 18mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20 difinf 9347 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴𝑥) ∈ Fin)
2119, 20sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴𝑥) ∈ Fin)
2221orcd 873 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
2322anim2i 617 . . . . . . . . . . . . . . . . . . . . . . . 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 3457 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2926, 28sylibr 234 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → 𝑥𝑇)
30 eleq1 2827 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = {𝑦} → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
31303ad2ant2 1133 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
3229, 31mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
3332sbcth 3806 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇))
348, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
35 sbcimg 3843 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
368, 35ax-mp 5 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
3734, 36mpbi 230 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38 sbc3an 3861 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
39 sbcg 3870 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
408, 39ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41403anbi1i 1156 . . . . . . . . . . . . . . . . . 18 (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
42 eqsbc1 3841 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
438, 42ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44433anbi2i 1157 . . . . . . . . . . . . . . . . . 18 ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
4538, 41, 443bitri 297 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
46 sbcg 3870 . . . . . . . . . . . . . . . . . . 19 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴))
478, 46ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴)
48473anbi3i 1158 . . . . . . . . . . . . . . . . 17 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
4945, 48bitri 275 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
50 sbcg 3870 . . . . . . . . . . . . . . . . 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 631 . . . . . . . . . . 11 𝐴 ∈ Fin → ((𝑦𝐴𝑢 = {𝑦}) ↔ ((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
5756exbidv 1919 . . . . . . . . . 10 𝐴 ∈ Fin → (∃𝑦(𝑦𝐴𝑢 = {𝑦}) ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
586, 57bitrid 283 . . . . . . . . 9 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59 anass 468 . . . . . . . . . . 11 (((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
6059exbii 1845 . . . . . . . . . 10 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
61 exsimpr 1867 . . . . . . . . . 10 (∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6260, 61sylbi 217 . . . . . . . . 9 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6358, 62biimtrdi 253 . . . . . . . 8 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦})))
64 ancom 460 . . . . . . . . . 10 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65 eleq1 2827 . . . . . . . . . . 11 (𝑢 = {𝑦} → (𝑢𝑇 ↔ {𝑦} ∈ 𝑇))
6665pm5.32i 574 . . . . . . . . . 10 ((𝑢 = {𝑦} ∧ 𝑢𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
6764, 66bitr4i 278 . . . . . . . . 9 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢𝑇))
6867exbii 1845 . . . . . . . 8 (∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇))
6963, 68imbitrdi 251 . . . . . . 7 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇)))
70 exsimpr 1867 . . . . . . 7 (∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇) → ∃𝑦 𝑢𝑇)
7169, 70syl6 35 . . . . . 6 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢𝑇))
72 ax5e 1910 . . . . . 6 (∃𝑦 𝑢𝑇𝑢𝑇)
7371, 72syl6 35 . . . . 5 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → 𝑢𝑇))
741, 2, 3, 73ssrd 4000 . . . 4 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75 eqid 2735 . . . . 5 {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
7675dissneq 37324 . . . 4 (({𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
7774, 76sylan 580 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78 nfielex 9305 . . . . 5 𝐴 ∈ Fin → ∃𝑦 𝑦𝐴)
7978adantr 480 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦𝐴)
80 difss 4146 . . . . . . 7 (𝐴 ∖ {𝑦}) ⊆ 𝐴
81 elfvex 6945 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82 difexg 5335 . . . . . . . 8 (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83 elpwg 4608 . . . . . . . 8 ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8481, 82, 833syl 18 . . . . . . 7 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8580, 84mpbiri 258 . . . . . 6 (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
8685adantl 481 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
87 difinf 9347 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
8817, 87mpan2 691 . . . . . . . . . . 11 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89 0fi 9081 . . . . . . . . . . . 12 ∅ ∈ Fin
90 eleq1 2827 . . . . . . . . . . . 12 ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
9189, 90mpbiri 258 . . . . . . . . . . 11 ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
9288, 91nsyl 140 . . . . . . . . . 10 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
9392ad2antrl 728 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94 vsnid 4668 . . . . . . . . . . . . . 14 𝑦 ∈ {𝑦}
95 inelcm 4471 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
9694, 95mpan2 691 . . . . . . . . . . . . 13 (𝑦𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97 disj4 4465 . . . . . . . . . . . . . 14 ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
9897necon2abii 2989 . . . . . . . . . . . . 13 ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
9996, 98sylibr 234 . . . . . . . . . . . 12 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
10099pssned 4111 . . . . . . . . . . 11 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101100adantr 480 . . . . . . . . . 10 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102101neneqd 2943 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
10393, 102jca 511 . . . . . . . 8 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104 pm4.56 990 . . . . . . . 8 ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105103, 104sylib 218 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
106 difeq2 4130 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
107106eleq1d 2824 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
108107notbid 318 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109 eqeq1 2739 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
110 eqeq1 2739 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
111109, 110orbi12d 918 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
112108, 111orbi12d 918 . . . . . . . . . . 11 (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
113112, 27elrab2 3698 . . . . . . . . . 10 ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
11485biantrurd 532 . . . . . . . . . 10 (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
115113, 114bitr4id 290 . . . . . . . . 9 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116 dfin4 4284 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117 inss2 4246 . . . . . . . . . . . 12 (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118 ssfi 9212 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
11917, 117, 118mp2an 692 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) ∈ Fin
120116, 119eqeltrri 2836 . . . . . . . . . 10 (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121 biortn 937 . . . . . . . . . 10 ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122120, 121ax-mp 5 . . . . . . . . 9 (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123115, 122bitr4di 289 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124123ad2antll 729 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125105, 124mtbird 325 . . . . . 6 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126125expcom 413 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127 nelneq2 2864 . . . . . 6 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128 eqcom 2742 . . . . . 6 (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129127, 128sylnibr 329 . . . . 5 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
13086, 126, 129syl6an 684 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ 𝑇 = 𝒫 𝐴))
13179, 130exellimddv 37328 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
13277, 131pm2.65da 817 . 2 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133132con4i 114 1 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wex 1776  wcel 2106  {cab 2712  wne 2938  wrex 3068  {crab 3433  Vcvv 3478  [wsbc 3791  cdif 3960  cin 3962  wss 3963  wpss 3964  c0 4339  𝒫 cpw 4605  {csn 4631  cfv 6563  Fincfn 8984  TopOnctopon 22932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-om 7888  df-1o 8505  df-en 8985  df-fin 8988  df-topgen 17490  df-top 22916  df-topon 22933
This theorem is referenced by:  topdifinffin  37331
  Copyright terms: Public domain W3C validator