| Step | Hyp | Ref
| Expression |
| 1 | | uneq2 4162 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 ∪ 𝑥) = (𝐴 ∪ ∅)) |
| 2 | 1 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈
Fin)) |
| 3 | 2 | imbi2d 340 |
. . 3
⊢ (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈
Fin))) |
| 4 | | uneq2 4162 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝑦)) |
| 5 | 4 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin)) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin))) |
| 7 | | uneq2 4162 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∪ 𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧}))) |
| 8 | 7 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
| 9 | 8 | imbi2d 340 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))) |
| 10 | | uneq2 4162 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝐵)) |
| 11 | 10 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝐵) ∈ Fin)) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin))) |
| 13 | | un0 4394 |
. . . . 5
⊢ (𝐴 ∪ ∅) = 𝐴 |
| 14 | 13 | eleq1i 2832 |
. . . 4
⊢ ((𝐴 ∪ ∅) ∈ Fin
↔ 𝐴 ∈
Fin) |
| 15 | 14 | biimpri 228 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈
Fin) |
| 16 | | snssi 4808 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐴 → {𝑧} ⊆ 𝐴) |
| 17 | | ssequn2 4189 |
. . . . . . . . . . . . . 14
⊢ ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴) |
| 18 | 17 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴) |
| 19 | 18 | uneq2d 4168 |
. . . . . . . . . . . 12
⊢ ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦 ∪ 𝐴)) |
| 20 | | un12 4173 |
. . . . . . . . . . . 12
⊢ (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧})) |
| 21 | | uncom 4158 |
. . . . . . . . . . . 12
⊢ (𝐴 ∪ 𝑦) = (𝑦 ∪ 𝐴) |
| 22 | 19, 20, 21 | 3eqtr4g 2802 |
. . . . . . . . . . 11
⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦)) |
| 23 | 16, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦)) |
| 24 | 23 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin)) |
| 25 | 24 | biimprd 248 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
| 26 | 25 | adantld 490 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
| 27 | | isfi 9016 |
. . . . . . . . . . 11
⊢ ((𝐴 ∪ 𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤) |
| 28 | 27 | biimpi 216 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ 𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤) |
| 29 | | r19.41v 3189 |
. . . . . . . . . . 11
⊢
(∃𝑤 ∈
ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) ↔ (∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) |
| 30 | | disjsn 4711 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴 ∪ 𝑦)) |
| 31 | | elun 4153 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦)) |
| 32 | 31 | notbii 320 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑧 ∈ (𝐴 ∪ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦)) |
| 33 | | pm4.56 991 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦)) |
| 34 | 32, 33 | bitr4i 278 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) |
| 35 | 30, 34 | sylbbr 236 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅) |
| 36 | | nnord 7895 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ω → Ord 𝑤) |
| 37 | | orddisj 6422 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑤 → (𝑤 ∩ {𝑤}) = ∅) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅) |
| 39 | | en2sn 9081 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤}) |
| 40 | 39 | el2v 3487 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑧} ≈ {𝑤} |
| 41 | | unen 9086 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) |
| 42 | 40, 41 | mpanl2 701 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) |
| 43 | 38, 42 | sylanr2 683 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) |
| 44 | 35, 43 | sylanr1 682 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) |
| 45 | 44 | 3impb 1115 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) |
| 46 | 45 | 3comr 1126 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) |
| 47 | 46 | 3expb 1121 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) |
| 48 | | unass 4172 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∪ 𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧})) |
| 49 | | df-suc 6390 |
. . . . . . . . . . . . . . . . 17
⊢ suc 𝑤 = (𝑤 ∪ {𝑤}) |
| 50 | | peano2 7912 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ω → suc 𝑤 ∈
ω) |
| 51 | 49, 50 | eqeltrrid 2846 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω) |
| 52 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))) |
| 53 | 52 | rspcev 3622 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣) |
| 54 | 51, 53 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣) |
| 55 | | isfi 9016 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣) |
| 56 | 54, 55 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin) |
| 57 | 48, 56 | eqeltrrid 2846 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
| 58 | 47, 57 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
| 59 | 58 | rexlimiva 3147 |
. . . . . . . . . . 11
⊢
(∃𝑤 ∈
ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
| 60 | 29, 59 | sylbir 235 |
. . . . . . . . . 10
⊢
((∃𝑤 ∈
ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
| 61 | 28, 60 | sylan 580 |
. . . . . . . . 9
⊢ (((𝐴 ∪ 𝑦) ∈ Fin ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
| 62 | 61 | ancoms 458 |
. . . . . . . 8
⊢ (((¬
𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
| 63 | 62 | expl 457 |
. . . . . . 7
⊢ (¬
𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
| 64 | 26, 63 | pm2.61i 182 |
. . . . . 6
⊢ ((¬
𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin) |
| 65 | 64 | ex 412 |
. . . . 5
⊢ (¬
𝑧 ∈ 𝑦 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)) |
| 66 | 65 | imim2d 57 |
. . . 4
⊢ (¬
𝑧 ∈ 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))) |
| 67 | 66 | adantl 481 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))) |
| 68 | 3, 6, 9, 12, 15, 67 | findcard2s 9205 |
. 2
⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin)) |
| 69 | 68 | impcom 407 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) |