Step | Hyp | Ref
| Expression |
1 | | diffi 8738 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑋}) ∈ Fin) |
2 | | isfi 8521 |
. . . 4
⊢ ((𝐴 ∖ {𝑋}) ∈ Fin ↔ ∃𝑚 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑚) |
3 | | simp3 1130 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (𝐴 ∖ {𝑋}) ≈ 𝑚) |
4 | | en2sn 8581 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω) → {𝑋} ≈ {𝑚}) |
5 | 4 | 3adant3 1124 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → {𝑋} ≈ {𝑚}) |
6 | | incom 4175 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ({𝑋} ∩ (𝐴 ∖ {𝑋})) |
7 | | disjdif 4417 |
. . . . . . . . . . . . 13
⊢ ({𝑋} ∩ (𝐴 ∖ {𝑋})) = ∅ |
8 | 6, 7 | eqtri 2841 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅) |
10 | | nnord 7577 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ω → Ord 𝑚) |
11 | | ordirr 6202 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑚 → ¬ 𝑚 ∈ 𝑚) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ω → ¬
𝑚 ∈ 𝑚) |
13 | | disjsn 4639 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∩ {𝑚}) = ∅ ↔ ¬ 𝑚 ∈ 𝑚) |
14 | 12, 13 | sylibr 235 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅) |
15 | 14 | 3ad2ant2 1126 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (𝑚 ∩ {𝑚}) = ∅) |
16 | | unen 8584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∖ {𝑋}) ≈ 𝑚 ∧ {𝑋} ≈ {𝑚}) ∧ (((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚})) |
17 | 3, 5, 9, 15, 16 | syl22anc 834 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚})) |
18 | | difsnid 4735 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐴 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) = 𝐴) |
19 | | df-suc 6190 |
. . . . . . . . . . . . . 14
⊢ suc 𝑚 = (𝑚 ∪ {𝑚}) |
20 | 19 | eqcomi 2827 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∪ {𝑚}) = suc 𝑚 |
21 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐴 → (𝑚 ∪ {𝑚}) = suc 𝑚) |
22 | 18, 21 | breq12d 5070 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐴 → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚}) ↔ 𝐴 ≈ suc 𝑚)) |
23 | 22 | 3ad2ant1 1125 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑚 ∪ {𝑚}) ↔ 𝐴 ≈ suc 𝑚)) |
24 | 17, 23 | mpbid 233 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → 𝐴 ≈ suc 𝑚) |
25 | | peano2 7591 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω → suc 𝑚 ∈
ω) |
26 | 25 | 3ad2ant2 1126 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → suc 𝑚 ∈ ω) |
27 | | cardennn 9400 |
. . . . . . . . 9
⊢ ((𝐴 ≈ suc 𝑚 ∧ suc 𝑚 ∈ ω) → (card‘𝐴) = suc 𝑚) |
28 | 24, 26, 27 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘𝐴) = suc 𝑚) |
29 | | cardennn 9400 |
. . . . . . . . . . 11
⊢ (((𝐴 ∖ {𝑋}) ≈ 𝑚 ∧ 𝑚 ∈ ω) → (card‘(𝐴 ∖ {𝑋})) = 𝑚) |
30 | 29 | ancoms 459 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘(𝐴 ∖ {𝑋})) = 𝑚) |
31 | 30 | 3adant1 1122 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘(𝐴 ∖ {𝑋})) = 𝑚) |
32 | | suceq 6249 |
. . . . . . . . 9
⊢
((card‘(𝐴
∖ {𝑋})) = 𝑚 → suc (card‘(𝐴 ∖ {𝑋})) = suc 𝑚) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → suc (card‘(𝐴 ∖ {𝑋})) = suc 𝑚) |
34 | 28, 33 | eqtr4d 2856 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋}))) |
35 | 34 | 3expib 1114 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → ((𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
36 | 35 | com12 32 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧ (𝐴 ∖ {𝑋}) ≈ 𝑚) → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
37 | 36 | rexlimiva 3278 |
. . . 4
⊢
(∃𝑚 ∈
ω (𝐴 ∖ {𝑋}) ≈ 𝑚 → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
38 | 2, 37 | sylbi 218 |
. . 3
⊢ ((𝐴 ∖ {𝑋}) ∈ Fin → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
39 | 1, 38 | syl 17 |
. 2
⊢ (𝐴 ∈ Fin → (𝑋 ∈ 𝐴 → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))) |
40 | 39 | imp 407 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋}))) |