| Step | Hyp | Ref
| Expression |
| 1 | | peano2 7912 |
. . . . 5
⊢ (𝑀 ∈ ω → suc 𝑀 ∈
ω) |
| 2 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = suc 𝑀 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ suc 𝑀)) |
| 3 | 2 | rspcev 3622 |
. . . . . 6
⊢ ((suc
𝑀 ∈ ω ∧
𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
| 4 | | isfi 9016 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
| 5 | 3, 4 | sylibr 234 |
. . . . 5
⊢ ((suc
𝑀 ∈ ω ∧
𝐴 ≈ suc 𝑀) → 𝐴 ∈ Fin) |
| 6 | 1, 5 | sylan 580 |
. . . 4
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) → 𝐴 ∈ Fin) |
| 7 | | diffi 9215 |
. . . . 5
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑋}) ∈ Fin) |
| 8 | | isfi 9016 |
. . . . 5
⊢ ((𝐴 ∖ {𝑋}) ∈ Fin ↔ ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
| 9 | 7, 8 | sylib 218 |
. . . 4
⊢ (𝐴 ∈ Fin → ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
| 10 | 6, 9 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
| 11 | 10 | 3adant3 1133 |
. 2
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
| 12 | | en2sn 9081 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑥 ∈ V) → {𝑋} ≈ {𝑥}) |
| 13 | 12 | elvd 3486 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐴 → {𝑋} ≈ {𝑥}) |
| 14 | | nnord 7895 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → Ord 𝑥) |
| 15 | | orddisj 6422 |
. . . . . . . 8
⊢ (Ord
𝑥 → (𝑥 ∩ {𝑥}) = ∅) |
| 16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ω → (𝑥 ∩ {𝑥}) = ∅) |
| 17 | | incom 4209 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ({𝑋} ∩ (𝐴 ∖ {𝑋})) |
| 18 | | disjdif 4472 |
. . . . . . . . . 10
⊢ ({𝑋} ∩ (𝐴 ∖ {𝑋})) = ∅ |
| 19 | 17, 18 | eqtri 2765 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ |
| 20 | | unen 9086 |
. . . . . . . . . 10
⊢ ((((𝐴 ∖ {𝑋}) ≈ 𝑥 ∧ {𝑋} ≈ {𝑥}) ∧ (((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥})) |
| 21 | 20 | an4s 660 |
. . . . . . . . 9
⊢ ((((𝐴 ∖ {𝑋}) ≈ 𝑥 ∧ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅) ∧ ({𝑋} ≈ {𝑥} ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥})) |
| 22 | 19, 21 | mpanl2 701 |
. . . . . . . 8
⊢ (((𝐴 ∖ {𝑋}) ≈ 𝑥 ∧ ({𝑋} ≈ {𝑥} ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥})) |
| 23 | 22 | expcom 413 |
. . . . . . 7
⊢ (({𝑋} ≈ {𝑥} ∧ (𝑥 ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}))) |
| 24 | 13, 16, 23 | syl2an 596 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}))) |
| 25 | 24 | 3ad2antl3 1188 |
. . . . 5
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}))) |
| 26 | | difsnid 4810 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐴 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) = 𝐴) |
| 27 | | df-suc 6390 |
. . . . . . . . . . 11
⊢ suc 𝑥 = (𝑥 ∪ {𝑥}) |
| 28 | 27 | eqcomi 2746 |
. . . . . . . . . 10
⊢ (𝑥 ∪ {𝑥}) = suc 𝑥 |
| 29 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐴 → (𝑥 ∪ {𝑥}) = suc 𝑥) |
| 30 | 26, 29 | breq12d 5156 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐴 → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) ↔ 𝐴 ≈ suc 𝑥)) |
| 31 | 30 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) ↔ 𝐴 ≈ suc 𝑥)) |
| 32 | 31 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) ↔ 𝐴 ≈ suc 𝑥)) |
| 33 | | ensym 9043 |
. . . . . . . . . . 11
⊢ (𝐴 ≈ suc 𝑀 → suc 𝑀 ≈ 𝐴) |
| 34 | | entr 9046 |
. . . . . . . . . . . . 13
⊢ ((suc
𝑀 ≈ 𝐴 ∧ 𝐴 ≈ suc 𝑥) → suc 𝑀 ≈ suc 𝑥) |
| 35 | | peano2 7912 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
| 36 | | nneneq 9246 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑀 ∈ ω ∧ suc
𝑥 ∈ ω) →
(suc 𝑀 ≈ suc 𝑥 ↔ suc 𝑀 = suc 𝑥)) |
| 37 | 35, 36 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
(suc 𝑀 ≈ suc 𝑥 ↔ suc 𝑀 = suc 𝑥)) |
| 38 | 34, 37 | imbitrid 244 |
. . . . . . . . . . . 12
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
((suc 𝑀 ≈ 𝐴 ∧ 𝐴 ≈ suc 𝑥) → suc 𝑀 = suc 𝑥)) |
| 39 | 38 | expd 415 |
. . . . . . . . . . 11
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
(suc 𝑀 ≈ 𝐴 → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥))) |
| 40 | 33, 39 | syl5 34 |
. . . . . . . . . 10
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
(𝐴 ≈ suc 𝑀 → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥))) |
| 41 | 1, 40 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 ≈ suc 𝑀 → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥))) |
| 42 | 41 | imp 406 |
. . . . . . . 8
⊢ (((𝑀 ∈ ω ∧ 𝑥 ∈ ω) ∧ 𝐴 ≈ suc 𝑀) → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥)) |
| 43 | 42 | an32s 652 |
. . . . . . 7
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) ∧ 𝑥 ∈ ω) → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥)) |
| 44 | 43 | 3adantl3 1169 |
. . . . . 6
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥)) |
| 45 | 32, 44 | sylbid 240 |
. . . . 5
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) → suc 𝑀 = suc 𝑥)) |
| 46 | | peano4 7914 |
. . . . . . 7
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (suc
𝑀 = suc 𝑥 ↔ 𝑀 = 𝑥)) |
| 47 | 46 | biimpd 229 |
. . . . . 6
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (suc
𝑀 = suc 𝑥 → 𝑀 = 𝑥)) |
| 48 | 47 | 3ad2antl1 1186 |
. . . . 5
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (suc 𝑀 = suc 𝑥 → 𝑀 = 𝑥)) |
| 49 | 25, 45, 48 | 3syld 60 |
. . . 4
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → 𝑀 = 𝑥)) |
| 50 | | breq2 5147 |
. . . . 5
⊢ (𝑀 = 𝑥 → ((𝐴 ∖ {𝑋}) ≈ 𝑀 ↔ (𝐴 ∖ {𝑋}) ≈ 𝑥)) |
| 51 | 50 | biimprcd 250 |
. . . 4
⊢ ((𝐴 ∖ {𝑋}) ≈ 𝑥 → (𝑀 = 𝑥 → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
| 52 | 49, 51 | sylcom 30 |
. . 3
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
| 53 | 52 | rexlimdva 3155 |
. 2
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥 → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
| 54 | 11, 53 | mpd 15 |
1
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |