| Step | Hyp | Ref
| Expression |
| 1 | | ssexg 5323 |
. . 3
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 ∈ V) |
| 2 | 1 | ancoms 458 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
| 3 | | sseq1 4009 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
| 4 | | eleq1 2829 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝑏 ∈ Fin ↔ 𝐵 ∈ Fin)) |
| 5 | 3, 4 | imbi12d 344 |
. . . . 5
⊢ (𝑏 = 𝐵 → ((𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin) ↔ (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))) |
| 6 | 5 | imbi2d 340 |
. . . 4
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) ↔ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))) |
| 7 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ∅)) |
| 8 | 7 | imbi1d 341 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin))) |
| 9 | 8 | albidv 1920 |
. . . . . 6
⊢ (𝑥 = ∅ → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin))) |
| 10 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝑦)) |
| 11 | 10 | imbi1d 341 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin))) |
| 12 | 11 | albidv 1920 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin))) |
| 13 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) |
| 14 | 13 | imbi1d 341 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))) |
| 15 | 14 | albidv 1920 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))) |
| 16 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝐴)) |
| 17 | 16 | imbi1d 341 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))) |
| 18 | 17 | albidv 1920 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑏(𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin) ↔ ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin))) |
| 19 | | ss0 4402 |
. . . . . . . 8
⊢ (𝑏 ⊆ ∅ → 𝑏 = ∅) |
| 20 | | 0fi 9082 |
. . . . . . . 8
⊢ ∅
∈ Fin |
| 21 | 19, 20 | eqeltrdi 2849 |
. . . . . . 7
⊢ (𝑏 ⊆ ∅ → 𝑏 ∈ Fin) |
| 22 | 21 | ax-gen 1795 |
. . . . . 6
⊢
∀𝑏(𝑏 ⊆ ∅ → 𝑏 ∈ Fin) |
| 23 | | sseq1 4009 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑐 → (𝑏 ⊆ 𝑦 ↔ 𝑐 ⊆ 𝑦)) |
| 24 | | eleq1w 2824 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑐 → (𝑏 ∈ Fin ↔ 𝑐 ∈ Fin)) |
| 25 | 23, 24 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑐 → ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ (𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin))) |
| 26 | 25 | cbvalvw 2035 |
. . . . . . . . 9
⊢
(∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) ↔ ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin)) |
| 27 | | simp1 1137 |
. . . . . . . . . . . . 13
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin)) |
| 28 | | snssi 4808 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑏 → {𝑧} ⊆ 𝑏) |
| 29 | | undif 4482 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑧} ⊆ 𝑏 ↔ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏) |
| 30 | 28, 29 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑏 → ({𝑧} ∪ (𝑏 ∖ {𝑧})) = 𝑏) |
| 31 | | uncom 4158 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑧} ∪ (𝑏 ∖ {𝑧})) = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) |
| 32 | 30, 31 | eqtr3di 2792 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑏 → 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) |
| 33 | | uncom 4158 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦) |
| 34 | 33 | sseq2i 4013 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑏 ⊆ ({𝑧} ∪ 𝑦)) |
| 35 | | ssundif 4488 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦) |
| 36 | 34, 35 | sylbb 219 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → (𝑏 ∖ {𝑧}) ⊆ 𝑦) |
| 37 | 32, 36 | anim12ci 614 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))) |
| 38 | 37 | 3adant1 1131 |
. . . . . . . . . . . . 13
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))) |
| 39 | | 3anass 1095 |
. . . . . . . . . . . . 13
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) ↔ (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})))) |
| 40 | 27, 38, 39 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → (∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}))) |
| 41 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑏 ∈ V |
| 42 | 41 | difexi 5330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∖ {𝑧}) ∈ V |
| 43 | | sseq1 4009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ⊆ 𝑦 ↔ (𝑏 ∖ {𝑧}) ⊆ 𝑦)) |
| 44 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑏 ∖ {𝑧}) → (𝑐 ∈ Fin ↔ (𝑏 ∖ {𝑧}) ∈ Fin)) |
| 45 | 43, 44 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑏 ∖ {𝑧}) → ((𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ↔ ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin))) |
| 46 | 42, 45 | spcv 3605 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑏 ∖ {𝑧}) ⊆ 𝑦 → (𝑏 ∖ {𝑧}) ∈ Fin)) |
| 47 | 46 | imp 406 |
. . . . . . . . . . . . . 14
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → (𝑏 ∖ {𝑧}) ∈ Fin) |
| 48 | | snfi 9083 |
. . . . . . . . . . . . . 14
⊢ {𝑧} ∈ Fin |
| 49 | | unfi 9211 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin) |
| 50 | 47, 48, 49 | sylancl 586 |
. . . . . . . . . . . . 13
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦) → ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin) |
| 51 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧}) → (𝑏 ∈ Fin ↔ ((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin)) |
| 52 | 51 | biimparc 479 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∖ {𝑧}) ∪ {𝑧}) ∈ Fin ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin) |
| 53 | 50, 52 | stoic3 1776 |
. . . . . . . . . . . 12
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ (𝑏 ∖ {𝑧}) ⊆ 𝑦 ∧ 𝑏 = ((𝑏 ∖ {𝑧}) ∪ {𝑧})) → 𝑏 ∈ Fin) |
| 54 | 40, 53 | syl 17 |
. . . . . . . . . . 11
⊢
((∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) |
| 55 | 54 | 3expib 1123 |
. . . . . . . . . 10
⊢
(∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) |
| 56 | 55 | alrimiv 1927 |
. . . . . . . . 9
⊢
(∀𝑐(𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) |
| 57 | 26, 56 | sylbi 217 |
. . . . . . . 8
⊢
(∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) |
| 58 | | disjsn 4711 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑏) |
| 59 | | disjssun 4468 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∩ {𝑧}) = ∅ → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦)) |
| 60 | 58, 59 | sylbir 235 |
. . . . . . . . . . . 12
⊢ (¬
𝑧 ∈ 𝑏 → (𝑏 ⊆ ({𝑧} ∪ 𝑦) ↔ 𝑏 ⊆ 𝑦)) |
| 61 | 60 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((¬
𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ({𝑧} ∪ 𝑦)) → 𝑏 ⊆ 𝑦) |
| 62 | 34, 61 | sylan2b 594 |
. . . . . . . . . 10
⊢ ((¬
𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ⊆ 𝑦) |
| 63 | 62 | imim1i 63 |
. . . . . . . . 9
⊢ ((𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) |
| 64 | 63 | alimi 1811 |
. . . . . . . 8
⊢
(∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) |
| 65 | | exmid 895 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) |
| 66 | 65 | jctl 523 |
. . . . . . . . . . 11
⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) |
| 67 | | andir 1011 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏) ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ↔ ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))) |
| 68 | 66, 67 | sylib 218 |
. . . . . . . . . 10
⊢ (𝑏 ⊆ (𝑦 ∪ {𝑧}) → ((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})))) |
| 69 | | pm3.44 962 |
. . . . . . . . . 10
⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) ∨ (¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧}))) → 𝑏 ∈ Fin)) |
| 70 | 68, 69 | syl5 34 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → (𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)) |
| 71 | 70 | alanimi 1816 |
. . . . . . . 8
⊢
((∀𝑏((𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin) ∧ ∀𝑏((¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ (𝑦 ∪ {𝑧})) → 𝑏 ∈ Fin)) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)) |
| 72 | 57, 64, 71 | syl2anc 584 |
. . . . . . 7
⊢
(∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin)) |
| 73 | 72 | a1i 11 |
. . . . . 6
⊢ (𝑦 ∈ Fin →
(∀𝑏(𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin) → ∀𝑏(𝑏 ⊆ (𝑦 ∪ {𝑧}) → 𝑏 ∈ Fin))) |
| 74 | 9, 12, 15, 18, 22, 73 | findcard2 9204 |
. . . . 5
⊢ (𝐴 ∈ Fin → ∀𝑏(𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) |
| 75 | 74 | 19.21bi 2189 |
. . . 4
⊢ (𝐴 ∈ Fin → (𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin)) |
| 76 | 6, 75 | vtoclg 3554 |
. . 3
⊢ (𝐵 ∈ V → (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))) |
| 77 | 76 | impd 410 |
. 2
⊢ (𝐵 ∈ V → ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)) |
| 78 | 2, 77 | mpcom 38 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) |