| Step | Hyp | Ref
| Expression |
| 1 | | diffi 9215 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑋}) ∈ Fin) |
| 2 | | isfi 9016 |
. . . 4
⊢ ((𝐴 ∖ {𝑋}) ∈ Fin ↔ ∃𝑚 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑚) |
| 3 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (𝐴 ∖ {𝑋}) ≈ 𝑚) |
| 4 | | en2sn 9081 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω) → {𝑋} ≈ {𝑚}) |
| 5 | 4 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → {𝑋} ≈ {𝑚}) |
| 6 | | disjdifr 4473 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ |
| 7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅) |
| 8 | | nnord 7895 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ω → Ord 𝑚) |
| 9 | | ordirr 6402 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑚 → ¬ 𝑚 ∈ 𝑚) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ω → ¬
𝑚 ∈ 𝑚) |
| 11 | | disjsn 4711 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∩ {𝑚}) = ∅ ↔ ¬ 𝑚 ∈ 𝑚) |
| 12 | 10, 11 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅) |
| 13 | 12 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (𝑚 ∩ {𝑚}) = ∅) |
| 14 | | unen 9086 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∖ {𝑋}) ≈ 𝑚 ∧ {𝑋} ≈ {𝑚}) ∧ (((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚})) |
| 15 | 3, 5, 7, 13, 14 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚})) |
| 16 | | difsnid 4810 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐴 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) = 𝐴) |
| 17 | | df-suc 6390 |
. . . . . . . . . . . . . 14
⊢ suc 𝑚 = (𝑚 ∪ {𝑚}) |
| 18 | 17 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∪ {𝑚}) = suc 𝑚 |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐴 → (𝑚 ∪ {𝑚}) = suc 𝑚) |
| 20 | 16, 19 | breq12d 5156 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐴 → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚}) ↔ 𝐴 ≈ suc 𝑚)) |
| 21 | 20 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚}) ↔ 𝐴 ≈ suc 𝑚)) |
| 22 | 15, 21 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → 𝐴 ≈ suc 𝑚) |
| 23 | | peano2 7912 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → suc 𝑚 ∈
ω) |
| 24 | 23 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → suc 𝑚 ∈ ω) |
| 25 | | cardennn 10023 |
. . . . . . . . 9
⊢ ((𝐴 ≈ suc 𝑚 ∧ suc 𝑚 ∈ ω) → (card‘𝐴) = suc 𝑚) |
| 26 | 22, 24, 25 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘𝐴) = suc 𝑚) |
| 27 | | cardennn 10023 |
. . . . . . . . . . 11
⊢ (((𝐴 ∖ {𝑋}) ≈ 𝑚 ∧ 𝑚 ∈ ω) → (card‘(𝐴 ∖ {𝑋})) = 𝑚) |
| 28 | 27 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘(𝐴 ∖ {𝑋})) = 𝑚) |
| 29 | 28 | 3adant1 1131 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘(𝐴 ∖ {𝑋})) = 𝑚) |
| 30 | | suceq 6450 |
. . . . . . . . 9
⊢
((card‘(𝐴
∖ {𝑋})) = 𝑚 → suc (card‘(𝐴 ∖ {𝑋})) = suc 𝑚) |
| 31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → suc (card‘(𝐴 ∖ {𝑋})) = suc 𝑚) |
| 32 | 26, 31 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋}))) |
| 33 | 32 | 3expib 1123 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → ((𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
| 34 | 33 | com12 32 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
| 35 | 34 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑚 ∈
ω (𝐴 ∖ {𝑋}) ≈ 𝑚 → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
| 36 | 2, 35 | sylbi 217 |
. . 3
⊢ ((𝐴 ∖ {𝑋}) ∈ Fin → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
| 37 | 1, 36 | syl 17 |
. 2
⊢ (𝐴 ∈ Fin → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
| 38 | 37 | imp 406 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋}))) |