Step | Hyp | Ref
| Expression |
1 | | diffi 9179 |
. . 3
β’ (π΄ β Fin β (π΄ β {π}) β Fin) |
2 | | isfi 8972 |
. . . 4
β’ ((π΄ β {π}) β Fin β βπ β Ο (π΄ β {π}) β π) |
3 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β (π΄ β {π}) β π) |
4 | | en2sn 9041 |
. . . . . . . . . . . 12
β’ ((π β π΄ β§ π β Ο) β {π} β {π}) |
5 | 4 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β {π} β {π}) |
6 | | disjdifr 4473 |
. . . . . . . . . . . 12
β’ ((π΄ β {π}) β© {π}) = β
|
7 | 6 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β ((π΄ β {π}) β© {π}) = β
) |
8 | | nnord 7863 |
. . . . . . . . . . . . . 14
β’ (π β Ο β Ord π) |
9 | | ordirr 6383 |
. . . . . . . . . . . . . 14
β’ (Ord
π β Β¬ π β π) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β Ο β Β¬
π β π) |
11 | | disjsn 4716 |
. . . . . . . . . . . . 13
β’ ((π β© {π}) = β
β Β¬ π β π) |
12 | 10, 11 | sylibr 233 |
. . . . . . . . . . . 12
β’ (π β Ο β (π β© {π}) = β
) |
13 | 12 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β (π β© {π}) = β
) |
14 | | unen 9046 |
. . . . . . . . . . 11
β’ ((((π΄ β {π}) β π β§ {π} β {π}) β§ (((π΄ β {π}) β© {π}) = β
β§ (π β© {π}) = β
)) β ((π΄ β {π}) βͺ {π}) β (π βͺ {π})) |
15 | 3, 5, 7, 13, 14 | syl22anc 838 |
. . . . . . . . . 10
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β ((π΄ β {π}) βͺ {π}) β (π βͺ {π})) |
16 | | difsnid 4814 |
. . . . . . . . . . . 12
β’ (π β π΄ β ((π΄ β {π}) βͺ {π}) = π΄) |
17 | | df-suc 6371 |
. . . . . . . . . . . . . 14
β’ suc π = (π βͺ {π}) |
18 | 17 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ (π βͺ {π}) = suc π |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π΄ β (π βͺ {π}) = suc π) |
20 | 16, 19 | breq12d 5162 |
. . . . . . . . . . 11
β’ (π β π΄ β (((π΄ β {π}) βͺ {π}) β (π βͺ {π}) β π΄ β suc π)) |
21 | 20 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β (((π΄ β {π}) βͺ {π}) β (π βͺ {π}) β π΄ β suc π)) |
22 | 15, 21 | mpbid 231 |
. . . . . . . . 9
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β π΄ β suc π) |
23 | | peano2 7881 |
. . . . . . . . . 10
β’ (π β Ο β suc π β
Ο) |
24 | 23 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β suc π β Ο) |
25 | | cardennn 9978 |
. . . . . . . . 9
β’ ((π΄ β suc π β§ suc π β Ο) β (cardβπ΄) = suc π) |
26 | 22, 24, 25 | syl2anc 585 |
. . . . . . . 8
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β (cardβπ΄) = suc π) |
27 | | cardennn 9978 |
. . . . . . . . . . 11
β’ (((π΄ β {π}) β π β§ π β Ο) β (cardβ(π΄ β {π})) = π) |
28 | 27 | ancoms 460 |
. . . . . . . . . 10
β’ ((π β Ο β§ (π΄ β {π}) β π) β (cardβ(π΄ β {π})) = π) |
29 | 28 | 3adant1 1131 |
. . . . . . . . 9
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β (cardβ(π΄ β {π})) = π) |
30 | | suceq 6431 |
. . . . . . . . 9
β’
((cardβ(π΄
β {π})) = π β suc (cardβ(π΄ β {π})) = suc π) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β suc (cardβ(π΄ β {π})) = suc π) |
32 | 26, 31 | eqtr4d 2776 |
. . . . . . 7
β’ ((π β π΄ β§ π β Ο β§ (π΄ β {π}) β π) β (cardβπ΄) = suc (cardβ(π΄ β {π}))) |
33 | 32 | 3expib 1123 |
. . . . . 6
β’ (π β π΄ β ((π β Ο β§ (π΄ β {π}) β π) β (cardβπ΄) = suc (cardβ(π΄ β {π})))) |
34 | 33 | com12 32 |
. . . . 5
β’ ((π β Ο β§ (π΄ β {π}) β π) β (π β π΄ β (cardβπ΄) = suc (cardβ(π΄ β {π})))) |
35 | 34 | rexlimiva 3148 |
. . . 4
β’
(βπ β
Ο (π΄ β {π}) β π β (π β π΄ β (cardβπ΄) = suc (cardβ(π΄ β {π})))) |
36 | 2, 35 | sylbi 216 |
. . 3
β’ ((π΄ β {π}) β Fin β (π β π΄ β (cardβπ΄) = suc (cardβ(π΄ β {π})))) |
37 | 1, 36 | syl 17 |
. 2
β’ (π΄ β Fin β (π β π΄ β (cardβπ΄) = suc (cardβ(π΄ β {π})))) |
38 | 37 | imp 408 |
1
β’ ((π΄ β Fin β§ π β π΄) β (cardβπ΄) = suc (cardβ(π΄ β {π}))) |