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 35818
Description: This is the core of the proof of topdifinffin 35819, 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 1917 . . . . 5 𝑢 ¬ 𝐴 ∈ Fin
2 nfab1 2909 . . . . 5 𝑢{𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
3 nfcv 2907 . . . . 5 𝑢𝑇
4 abid 2717 . . . . . . . . . . 11 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦𝐴 𝑢 = {𝑦})
5 df-rex 3074 . . . . . . . . . . 11 (∃𝑦𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
64, 5bitri 274 . . . . . . . . . 10 (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦𝐴𝑢 = {𝑦}))
7 eqid 2736 . . . . . . . . . . . . . . 15 {𝑦} = {𝑦}
8 vsnex 5386 . . . . . . . . . . . . . . . . . 18 {𝑦} ∈ V
9 snelpwi 5400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
10 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴))
119, 10syl5ibr 245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = {𝑦} → (𝑦𝐴𝑥 ∈ 𝒫 𝐴))
1211imdistani 569 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
1312anim2i 617 . . . . . . . . . . . . . . . . . . . . . . . 24 ((¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
14133impb 1115 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
15 3anass 1095 . . . . . . . . . . . . . . . . . . . . . . 23 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)))
1614, 15sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))
17 snfi 8988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑦} ∈ Fin
18 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin))
1917, 18mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = {𝑦} → 𝑥 ∈ Fin)
20 difinf 9260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ 𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴𝑥) ∈ Fin)
2119, 20sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴𝑥) ∈ Fin)
2221orcd 871 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))
2322anim2i 617 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2423ancoms 459 . . . . . . . . . . . . . . . . . . . . . . 23 (((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
25243impa 1110 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2616, 25syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
27 topdifinf.t . . . . . . . . . . . . . . . . . . . . . 22 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
2827reqabi 3429 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))))
2926, 28sylibr 233 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → 𝑥𝑇)
30 eleq1 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = {𝑦} → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
31303ad2ant2 1134 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → (𝑥𝑇 ↔ {𝑦} ∈ 𝑇))
3229, 31mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
3332sbcth 3754 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇))
348, 33ax-mp 5 . . . . . . . . . . . . . . . . 17 [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
35 sbcimg 3790 . . . . . . . . . . . . . . . . . 18 ({𝑦} ∈ V → ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)))
368, 35ax-mp 5 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))
3734, 36mpbi 229 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)
38 sbc3an 3809 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
39 sbcg 3818 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin))
408, 39ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)
41403anbi1i 1157 . . . . . . . . . . . . . . . . . 18 (([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
42 eqsbc1 3788 . . . . . . . . . . . . . . . . . . . 20 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}))
438, 42ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})
44433anbi2i 1158 . . . . . . . . . . . . . . . . . 18 ((¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
4538, 41, 443bitri 296 . . . . . . . . . . . . . . . . 17 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴))
46 sbcg 3818 . . . . . . . . . . . . . . . . . . 19 ({𝑦} ∈ V → ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴))
478, 46ax-mp 5 . . . . . . . . . . . . . . . . . 18 ([{𝑦} / 𝑥]𝑦𝐴𝑦𝐴)
48473anbi3i 1159 . . . . . . . . . . . . . . . . 17 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
4945, 48bitri 274 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴))
50 sbcg 3818 . . . . . . . . . . . . . . . . 17 ({𝑦} ∈ V → ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇))
518, 50ax-mp 5 . . . . . . . . . . . . . . . 16 ([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)
5237, 49, 513imtr3i 290 . . . . . . . . . . . . . . 15 ((¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
537, 52mp3an2 1449 . . . . . . . . . . . . . 14 ((¬ 𝐴 ∈ Fin ∧ 𝑦𝐴) → {𝑦} ∈ 𝑇)
5453ex 413 . . . . . . . . . . . . 13 𝐴 ∈ Fin → (𝑦𝐴 → {𝑦} ∈ 𝑇))
5554pm4.71d 562 . . . . . . . . . . . 12 𝐴 ∈ Fin → (𝑦𝐴 ↔ (𝑦𝐴 ∧ {𝑦} ∈ 𝑇)))
5655anbi1d 630 . . . . . . . . . . 11 𝐴 ∈ Fin → ((𝑦𝐴𝑢 = {𝑦}) ↔ ((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
5756exbidv 1924 . . . . . . . . . 10 𝐴 ∈ Fin → (∃𝑦(𝑦𝐴𝑢 = {𝑦}) ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
586, 57bitrid 282 . . . . . . . . 9 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦})))
59 anass 469 . . . . . . . . . . 11 (((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
6059exbii 1850 . . . . . . . . . 10 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})))
61 exsimpr 1872 . . . . . . . . . 10 (∃𝑦(𝑦𝐴 ∧ ({𝑦} ∈ 𝑇𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6260, 61sylbi 216 . . . . . . . . 9 (∃𝑦((𝑦𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}))
6358, 62syl6bi 252 . . . . . . . 8 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦})))
64 ancom 461 . . . . . . . . . 10 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
65 eleq1 2825 . . . . . . . . . . 11 (𝑢 = {𝑦} → (𝑢𝑇 ↔ {𝑦} ∈ 𝑇))
6665pm5.32i 575 . . . . . . . . . 10 ((𝑢 = {𝑦} ∧ 𝑢𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇))
6764, 66bitr4i 277 . . . . . . . . 9 (({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢𝑇))
6867exbii 1850 . . . . . . . 8 (∃𝑦({𝑦} ∈ 𝑇𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇))
6963, 68syl6ib 250 . . . . . . 7 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇)))
70 exsimpr 1872 . . . . . . 7 (∃𝑦(𝑢 = {𝑦} ∧ 𝑢𝑇) → ∃𝑦 𝑢𝑇)
7169, 70syl6 35 . . . . . 6 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢𝑇))
72 ax5e 1915 . . . . . 6 (∃𝑦 𝑢𝑇𝑢𝑇)
7371, 72syl6 35 . . . . 5 𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} → 𝑢𝑇))
741, 2, 3, 73ssrd 3949 . . . 4 𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇)
75 eqid 2736 . . . . 5 {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}}
7675dissneq 35812 . . . 4 (({𝑢 ∣ ∃𝑦𝐴 𝑢 = {𝑦}} ⊆ 𝑇𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
7774, 76sylan 580 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴)
78 nfielex 9217 . . . . 5 𝐴 ∈ Fin → ∃𝑦 𝑦𝐴)
7978adantr 481 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦𝐴)
80 difss 4091 . . . . . . 7 (𝐴 ∖ {𝑦}) ⊆ 𝐴
81 elfvex 6880 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V)
82 difexg 5284 . . . . . . . 8 (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V)
83 elpwg 4563 . . . . . . . 8 ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8481, 82, 833syl 18 . . . . . . 7 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴))
8580, 84mpbiri 257 . . . . . 6 (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
8685adantl 482 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴)
87 difinf 9260 . . . . . . . . . . . 12 ((¬ 𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
8817, 87mpan2 689 . . . . . . . . . . 11 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) ∈ Fin)
89 0fin 9115 . . . . . . . . . . . 12 ∅ ∈ Fin
90 eleq1 2825 . . . . . . . . . . . 12 ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈ Fin))
9189, 90mpbiri 257 . . . . . . . . . . 11 ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin)
9288, 91nsyl 140 . . . . . . . . . 10 𝐴 ∈ Fin → ¬ (𝐴 ∖ {𝑦}) = ∅)
9392ad2antrl 726 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅)
94 vsnid 4623 . . . . . . . . . . . . . 14 𝑦 ∈ {𝑦}
95 inelcm 4424 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅)
9694, 95mpan2 689 . . . . . . . . . . . . 13 (𝑦𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅)
97 disj4 4418 . . . . . . . . . . . . . 14 ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴)
9897necon2abii 2994 . . . . . . . . . . . . 13 ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅)
9996, 98sylibr 233 . . . . . . . . . . . 12 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴)
10099pssned 4058 . . . . . . . . . . 11 (𝑦𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴)
101100adantr 481 . . . . . . . . . 10 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴)
102101neneqd 2948 . . . . . . . . 9 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴)
10393, 102jca 512 . . . . . . . 8 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴))
104 pm4.56 987 . . . . . . . 8 ((¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
105103, 104sylib 217 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))
106 difeq2 4076 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
107106eleq1d 2822 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
108107notbid 317 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
109 eqeq1 2740 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅))
110 eqeq1 2740 . . . . . . . . . . . . 13 (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴))
111109, 110orbi12d 917 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
112108, 111orbi12d 917 . . . . . . . . . . 11 (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
113112, 27elrab2 3648 . . . . . . . . . 10 ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
11485biantrurd 533 . . . . . . . . . 10 (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))))
115113, 114bitr4id 289 . . . . . . . . 9 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
116 dfin4 4227 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦}))
117 inss2 4189 . . . . . . . . . . . 12 (𝐴 ∩ {𝑦}) ⊆ {𝑦}
118 ssfi 9117 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin)
11917, 117, 118mp2an 690 . . . . . . . . . . 11 (𝐴 ∩ {𝑦}) ∈ Fin
120116, 119eqeltrri 2835 . . . . . . . . . 10 (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
121 biortn 936 . . . . . . . . . 10 ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))
122120, 121ax-mp 5 . . . . . . . . 9 (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
123115, 122bitr4di 288 . . . . . . . 8 (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
124123ad2antll 727 . . . . . . 7 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))
125105, 124mtbird 324 . . . . . 6 ((𝑦𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)
126125expcom 414 . . . . 5 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇))
127 nelneq2 2862 . . . . . 6 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇)
128 eqcom 2743 . . . . . 6 (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇)
129127, 128sylnibr 328 . . . . 5 (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴)
13086, 126, 129syl6an 682 . . . 4 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦𝐴 → ¬ 𝑇 = 𝒫 𝐴))
13179, 130exellimddv 35816 . . 3 ((¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴)
13277, 131pm2.65da 815 . 2 𝐴 ∈ Fin → ¬ 𝑇 ∈ (TopOn‘𝐴))
133132con4i 114 1 (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wne 2943  wrex 3073  {crab 3407  Vcvv 3445  [wsbc 3739  cdif 3907  cin 3909  wss 3910  wpss 3911  c0 4282  𝒫 cpw 4560  {csn 4586  cfv 6496  Fincfn 8883  TopOnctopon 22259
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-1o 8412  df-en 8884  df-fin 8887  df-topgen 17325  df-top 22243  df-topon 22260
This theorem is referenced by:  topdifinffin  35819
  Copyright terms: Public domain W3C validator