| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑢 ¬ 𝐴 ∈ Fin | 
| 2 |  | nfab1 2906 | . . . . 5
⊢
Ⅎ𝑢{𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} | 
| 3 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑢𝑇 | 
| 4 |  | abid 2717 | . . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}) | 
| 5 |  | df-rex 3070 | . . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝐴 𝑢 = {𝑦} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦})) | 
| 6 | 4, 5 | bitri 275 | . . . . . . . . . 10
⊢ (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦})) | 
| 7 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ {𝑦} = {𝑦} | 
| 8 |  | vsnex 5433 | . . . . . . . . . . . . . . . . . 18
⊢ {𝑦} ∈ V | 
| 9 |  | snelpwi 5447 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴) | 
| 10 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝒫 𝐴 ↔ {𝑦} ∈ 𝒫 𝐴)) | 
| 11 | 9, 10 | imbitrrid 246 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = {𝑦} → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴)) | 
| 12 | 11 | imdistani 568 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)) | 
| 13 | 12 | anim2i 617 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴)) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))) | 
| 14 | 13 | 3impb 1114 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))) | 
| 15 |  | 3anass 1094 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ (𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴))) | 
| 16 | 14, 15 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴)) | 
| 17 |  | snfi 9084 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {𝑦} ∈ Fin | 
| 18 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = {𝑦} → (𝑥 ∈ Fin ↔ {𝑦} ∈ Fin)) | 
| 19 | 17, 18 | mpbiri 258 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = {𝑦} → 𝑥 ∈ Fin) | 
| 20 |  | difinf 9350 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 ∈ Fin) → ¬ (𝐴 ∖ 𝑥) ∈ Fin) | 
| 21 | 19, 20 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → ¬ (𝐴 ∖ 𝑥) ∈ Fin) | 
| 22 | 21 | orcd 873 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))) | 
| 23 | 22 | anim2i 617 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦})) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))) | 
| 24 | 23 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦}) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))) | 
| 25 | 24 | 3impa 1109 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))) | 
| 26 | 16, 25 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))) | 
| 27 |  | topdifinf.t | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))} | 
| 28 | 27 | reqabi 3459 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝑇 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))) | 
| 29 | 26, 28 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝑇) | 
| 30 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = {𝑦} → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)) | 
| 31 | 30 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)) | 
| 32 | 29, 31 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) | 
| 33 | 32 | sbcth 3802 | . . . . . . . . . . . . . . . . . 18
⊢ ({𝑦} ∈ V → [{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇)) | 
| 34 | 8, 33 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
[{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) | 
| 35 |  | sbcimg 3836 | . . . . . . . . . . . . . . . . . 18
⊢ ({𝑦} ∈ V →
([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇))) | 
| 36 | 8, 35 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
([{𝑦} / 𝑥]((¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) ↔ ([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇)) | 
| 37 | 34, 36 | mpbi 230 | . . . . . . . . . . . . . . . 16
⊢
([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) → [{𝑦} / 𝑥]{𝑦} ∈ 𝑇) | 
| 38 |  | sbc3an 3854 | . . . . . . . . . . . . . . . . . 18
⊢
([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ ([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴)) | 
| 39 |  | sbcg 3862 | . . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑦} ∈ V →
([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin)) | 
| 40 | 8, 39 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢
([{𝑦} / 𝑥] ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ∈ Fin) | 
| 41 | 40 | 3anbi1i 1157 | . . . . . . . . . . . . . . . . . 18
⊢
(([{𝑦} /
𝑥] ¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ [{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴)) | 
| 42 |  | eqsbc1 3834 | . . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑦} ∈ V →
([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦})) | 
| 43 | 8, 42 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢
([{𝑦} / 𝑥]𝑥 = {𝑦} ↔ {𝑦} = {𝑦}) | 
| 44 | 43 | 3anbi2i 1158 | . . . . . . . . . . . . . . . . . 18
⊢ ((¬
𝐴 ∈ Fin ∧
[{𝑦} / 𝑥]𝑥 = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴)) | 
| 45 | 38, 41, 44 | 3bitri 297 | . . . . . . . . . . . . . . . . 17
⊢
([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴)) | 
| 46 |  | sbcg 3862 | . . . . . . . . . . . . . . . . . . 19
⊢ ({𝑦} ∈ V →
([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | 
| 47 | 8, 46 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢
([{𝑦} / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | 
| 48 | 47 | 3anbi3i 1159 | . . . . . . . . . . . . . . . . 17
⊢ ((¬
𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ [{𝑦} / 𝑥]𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴)) | 
| 49 | 45, 48 | bitri 275 | . . . . . . . . . . . . . . . 16
⊢
([{𝑦} / 𝑥](¬ 𝐴 ∈ Fin ∧ 𝑥 = {𝑦} ∧ 𝑦 ∈ 𝐴) ↔ (¬ 𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴)) | 
| 50 |  | sbcg 3862 | . . . . . . . . . . . . . . . . 17
⊢ ({𝑦} ∈ V →
([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)) | 
| 51 | 8, 50 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢
([{𝑦} / 𝑥]{𝑦} ∈ 𝑇 ↔ {𝑦} ∈ 𝑇) | 
| 52 | 37, 49, 51 | 3imtr3i 291 | . . . . . . . . . . . . . . 15
⊢ ((¬
𝐴 ∈ Fin ∧ {𝑦} = {𝑦} ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) | 
| 53 | 7, 52 | mp3an2 1450 | . . . . . . . . . . . . . 14
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑦 ∈ 𝐴) → {𝑦} ∈ 𝑇) | 
| 54 | 53 | ex 412 | . . . . . . . . . . . . 13
⊢ (¬
𝐴 ∈ Fin → (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝑇)) | 
| 55 | 54 | pm4.71d 561 | . . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ Fin → (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇))) | 
| 56 | 55 | anbi1d 631 | . . . . . . . . . . 11
⊢ (¬
𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}))) | 
| 57 | 56 | exbidv 1920 | . . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin →
(∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}))) | 
| 58 | 6, 57 | bitrid 283 | . . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ↔ ∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}))) | 
| 59 |  | anass 468 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ (𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))) | 
| 60 | 59 | exbii 1847 | . . . . . . . . . 10
⊢
(∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))) | 
| 61 |  | exsimpr 1868 | . . . . . . . . . 10
⊢
(∃𝑦(𝑦 ∈ 𝐴 ∧ ({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})) | 
| 62 | 60, 61 | sylbi 217 | . . . . . . . . 9
⊢
(∃𝑦((𝑦 ∈ 𝐴 ∧ {𝑦} ∈ 𝑇) ∧ 𝑢 = {𝑦}) → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦})) | 
| 63 | 58, 62 | biimtrdi 253 | . . . . . . . 8
⊢ (¬
𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}))) | 
| 64 |  | ancom 460 | . . . . . . . . . 10
⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇)) | 
| 65 |  | eleq1 2828 | . . . . . . . . . . 11
⊢ (𝑢 = {𝑦} → (𝑢 ∈ 𝑇 ↔ {𝑦} ∈ 𝑇)) | 
| 66 | 65 | pm5.32i 574 | . . . . . . . . . 10
⊢ ((𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) ↔ (𝑢 = {𝑦} ∧ {𝑦} ∈ 𝑇)) | 
| 67 | 64, 66 | bitr4i 278 | . . . . . . . . 9
⊢ (({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ (𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇)) | 
| 68 | 67 | exbii 1847 | . . . . . . . 8
⊢
(∃𝑦({𝑦} ∈ 𝑇 ∧ 𝑢 = {𝑦}) ↔ ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇)) | 
| 69 | 63, 68 | imbitrdi 251 | . . . . . . 7
⊢ (¬
𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇))) | 
| 70 |  | exsimpr 1868 | . . . . . . 7
⊢
(∃𝑦(𝑢 = {𝑦} ∧ 𝑢 ∈ 𝑇) → ∃𝑦 𝑢 ∈ 𝑇) | 
| 71 | 69, 70 | syl6 35 | . . . . . 6
⊢ (¬
𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → ∃𝑦 𝑢 ∈ 𝑇)) | 
| 72 |  | ax5e 1911 | . . . . . 6
⊢
(∃𝑦 𝑢 ∈ 𝑇 → 𝑢 ∈ 𝑇) | 
| 73 | 71, 72 | syl6 35 | . . . . 5
⊢ (¬
𝐴 ∈ Fin → (𝑢 ∈ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} → 𝑢 ∈ 𝑇)) | 
| 74 | 1, 2, 3, 73 | ssrd 3987 | . . . 4
⊢ (¬
𝐴 ∈ Fin → {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇) | 
| 75 |  | eqid 2736 | . . . . 5
⊢ {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} = {𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} | 
| 76 | 75 | dissneq 37343 | . . . 4
⊢ (({𝑢 ∣ ∃𝑦 ∈ 𝐴 𝑢 = {𝑦}} ⊆ 𝑇 ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴) | 
| 77 | 74, 76 | sylan 580 | . . 3
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → 𝑇 = 𝒫 𝐴) | 
| 78 |  | nfielex 9308 | . . . . 5
⊢ (¬
𝐴 ∈ Fin →
∃𝑦 𝑦 ∈ 𝐴) | 
| 79 | 78 | adantr 480 | . . . 4
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ∃𝑦 𝑦 ∈ 𝐴) | 
| 80 |  | difss 4135 | . . . . . . 7
⊢ (𝐴 ∖ {𝑦}) ⊆ 𝐴 | 
| 81 |  | elfvex 6943 | . . . . . . . 8
⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ V) | 
| 82 |  | difexg 5328 | . . . . . . . 8
⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑦}) ∈ V) | 
| 83 |  | elpwg 4602 | . . . . . . . 8
⊢ ((𝐴 ∖ {𝑦}) ∈ V → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴)) | 
| 84 | 81, 82, 83 | 3syl 18 | . . . . . . 7
⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝐴)) | 
| 85 | 80, 84 | mpbiri 258 | . . . . . 6
⊢ (𝑇 ∈ (TopOn‘𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴) | 
| 86 | 85 | adantl 481 | . . . . 5
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴) | 
| 87 |  | difinf 9350 | . . . . . . . . . . . 12
⊢ ((¬
𝐴 ∈ Fin ∧ {𝑦} ∈ Fin) → ¬
(𝐴 ∖ {𝑦}) ∈ Fin) | 
| 88 | 17, 87 | mpan2 691 | . . . . . . . . . . 11
⊢ (¬
𝐴 ∈ Fin → ¬
(𝐴 ∖ {𝑦}) ∈ Fin) | 
| 89 |  | 0fi 9083 | . . . . . . . . . . . 12
⊢ ∅
∈ Fin | 
| 90 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ ((𝐴 ∖ {𝑦}) = ∅ → ((𝐴 ∖ {𝑦}) ∈ Fin ↔ ∅ ∈
Fin)) | 
| 91 | 89, 90 | mpbiri 258 | . . . . . . . . . . 11
⊢ ((𝐴 ∖ {𝑦}) = ∅ → (𝐴 ∖ {𝑦}) ∈ Fin) | 
| 92 | 88, 91 | nsyl 140 | . . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin → ¬
(𝐴 ∖ {𝑦}) = ∅) | 
| 93 | 92 | ad2antrl 728 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = ∅) | 
| 94 |  | vsnid 4662 | . . . . . . . . . . . . . 14
⊢ 𝑦 ∈ {𝑦} | 
| 95 |  | inelcm 4464 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ {𝑦}) → (𝐴 ∩ {𝑦}) ≠ ∅) | 
| 96 | 94, 95 | mpan2 691 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 → (𝐴 ∩ {𝑦}) ≠ ∅) | 
| 97 |  | disj4 4458 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∩ {𝑦}) = ∅ ↔ ¬ (𝐴 ∖ {𝑦}) ⊊ 𝐴) | 
| 98 | 97 | necon2abii 2990 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∖ {𝑦}) ⊊ 𝐴 ↔ (𝐴 ∩ {𝑦}) ≠ ∅) | 
| 99 | 96, 98 | sylibr 234 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ⊊ 𝐴) | 
| 100 | 99 | pssned 4100 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → (𝐴 ∖ {𝑦}) ≠ 𝐴) | 
| 101 | 100 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (𝐴 ∖ {𝑦}) ≠ 𝐴) | 
| 102 | 101 | neneqd 2944 | . . . . . . . . 9
⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) = 𝐴) | 
| 103 | 93, 102 | jca 511 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → (¬ (𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴)) | 
| 104 |  | pm4.56 990 | . . . . . . . 8
⊢ ((¬
(𝐴 ∖ {𝑦}) = ∅ ∧ ¬ (𝐴 ∖ {𝑦}) = 𝐴) ↔ ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) | 
| 105 | 103, 104 | sylib 218 | . . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) | 
| 106 |  | difeq2 4119 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦}))) | 
| 107 | 106 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)) | 
| 108 | 107 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (¬ (𝐴 ∖ 𝑥) ∈ Fin ↔ ¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)) | 
| 109 |  | eqeq1 2740 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = ∅ ↔ (𝐴 ∖ {𝑦}) = ∅)) | 
| 110 |  | eqeq1 2740 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → (𝑥 = 𝐴 ↔ (𝐴 ∖ {𝑦}) = 𝐴)) | 
| 111 | 109, 110 | orbi12d 918 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))) | 
| 112 | 108, 111 | orbi12d 918 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐴 ∖ {𝑦}) → ((¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))) | 
| 113 | 112, 27 | elrab2 3694 | . . . . . . . . . 10
⊢ ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))) | 
| 114 | 85 | biantrurd 532 | . . . . . . . . . 10
⊢ (𝑇 ∈ (TopOn‘𝐴) → ((¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)) ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))))) | 
| 115 | 113, 114 | bitr4id 290 | . . . . . . . . 9
⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))) | 
| 116 |  | dfin4 4277 | . . . . . . . . . . 11
⊢ (𝐴 ∩ {𝑦}) = (𝐴 ∖ (𝐴 ∖ {𝑦})) | 
| 117 |  | inss2 4237 | . . . . . . . . . . . 12
⊢ (𝐴 ∩ {𝑦}) ⊆ {𝑦} | 
| 118 |  | ssfi 9214 | . . . . . . . . . . . 12
⊢ (({𝑦} ∈ Fin ∧ (𝐴 ∩ {𝑦}) ⊆ {𝑦}) → (𝐴 ∩ {𝑦}) ∈ Fin) | 
| 119 | 17, 117, 118 | mp2an 692 | . . . . . . . . . . 11
⊢ (𝐴 ∩ {𝑦}) ∈ Fin | 
| 120 | 116, 119 | eqeltrri 2837 | . . . . . . . . . 10
⊢ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin | 
| 121 |  | biortn 937 | . . . . . . . . . 10
⊢ ((𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin → (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴)))) | 
| 122 | 120, 121 | ax-mp 5 | . . . . . . . . 9
⊢ (((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴) ↔ (¬ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin ∨ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))) | 
| 123 | 115, 122 | bitr4di 289 | . . . . . . . 8
⊢ (𝑇 ∈ (TopOn‘𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))) | 
| 124 | 123 | ad2antll 729 | . . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ((𝐴 ∖ {𝑦}) ∈ 𝑇 ↔ ((𝐴 ∖ {𝑦}) = ∅ ∨ (𝐴 ∖ {𝑦}) = 𝐴))) | 
| 125 | 105, 124 | mtbird 325 | . . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴))) → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) | 
| 126 | 125 | expcom 413 | . . . . 5
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇)) | 
| 127 |  | nelneq2 2865 | . . . . . 6
⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝒫 𝐴 = 𝑇) | 
| 128 |  | eqcom 2743 | . . . . . 6
⊢ (𝑇 = 𝒫 𝐴 ↔ 𝒫 𝐴 = 𝑇) | 
| 129 | 127, 128 | sylnibr 329 | . . . . 5
⊢ (((𝐴 ∖ {𝑦}) ∈ 𝒫 𝐴 ∧ ¬ (𝐴 ∖ {𝑦}) ∈ 𝑇) → ¬ 𝑇 = 𝒫 𝐴) | 
| 130 | 86, 126, 129 | syl6an 684 | . . . 4
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → (𝑦 ∈ 𝐴 → ¬ 𝑇 = 𝒫 𝐴)) | 
| 131 | 79, 130 | exellimddv 37347 | . . 3
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑇 ∈ (TopOn‘𝐴)) → ¬ 𝑇 = 𝒫 𝐴) | 
| 132 | 77, 131 | pm2.65da 816 | . 2
⊢ (¬
𝐴 ∈ Fin → ¬
𝑇 ∈ (TopOn‘𝐴)) | 
| 133 | 132 | con4i 114 | 1
⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin) |