Step | Hyp | Ref
| Expression |
1 | | peano2 7831 |
. . . . . . 7
β’ (π΄ β Ο β suc π΄ β
Ο) |
2 | | pw2eng 9028 |
. . . . . . 7
β’ (suc
π΄ β Ο β
π« suc π΄ β
(2o βm suc π΄)) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π΄ β Ο β π«
suc π΄ β
(2o βm suc π΄)) |
4 | | df-suc 6327 |
. . . . . . . . . 10
β’ suc π΄ = (π΄ βͺ {π΄}) |
5 | 4 | oveq2i 7372 |
. . . . . . . . 9
β’
(2o βm suc π΄) = (2o βm (π΄ βͺ {π΄})) |
6 | | elex 3465 |
. . . . . . . . . . 11
β’ (π΄ β Ο β π΄ β V) |
7 | | snex 5392 |
. . . . . . . . . . . 12
β’ {π΄} β V |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
β’ (π΄ β Ο β {π΄} β V) |
9 | | 2onn 8592 |
. . . . . . . . . . . . 13
β’
2o β Ο |
10 | 9 | elexi 3466 |
. . . . . . . . . . . 12
β’
2o β V |
11 | 10 | a1i 11 |
. . . . . . . . . . 11
β’ (π΄ β Ο β
2o β V) |
12 | | nnord 7814 |
. . . . . . . . . . . 12
β’ (π΄ β Ο β Ord π΄) |
13 | | orddisj 6359 |
. . . . . . . . . . . 12
β’ (Ord
π΄ β (π΄ β© {π΄}) = β
) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
β’ (π΄ β Ο β (π΄ β© {π΄}) = β
) |
15 | | mapunen 9096 |
. . . . . . . . . . 11
β’ (((π΄ β V β§ {π΄} β V β§ 2o
β V) β§ (π΄ β©
{π΄}) = β
) β
(2o βm (π΄ βͺ {π΄})) β ((2o
βm π΄)
Γ (2o βm {π΄}))) |
16 | 6, 8, 11, 14, 15 | syl31anc 1374 |
. . . . . . . . . 10
β’ (π΄ β Ο β
(2o βm (π΄ βͺ {π΄})) β ((2o
βm π΄)
Γ (2o βm {π΄}))) |
17 | | ovex 7394 |
. . . . . . . . . . . 12
β’
(2o βm π΄) β V |
18 | 17 | enref 8931 |
. . . . . . . . . . 11
β’
(2o βm π΄) β (2o βm
π΄) |
19 | | 2on 8430 |
. . . . . . . . . . . . 13
β’
2o β On |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
β’ (π΄ β Ο β
2o β On) |
21 | | id 22 |
. . . . . . . . . . . 12
β’ (π΄ β Ο β π΄ β
Ο) |
22 | 20, 21 | mapsnend 8986 |
. . . . . . . . . . 11
β’ (π΄ β Ο β
(2o βm {π΄}) β 2o) |
23 | | xpen 9090 |
. . . . . . . . . . 11
β’
(((2o βm π΄) β (2o βm
π΄) β§ (2o
βm {π΄})
β 2o) β ((2o βm π΄) Γ (2o
βm {π΄}))
β ((2o βm π΄) Γ 2o)) |
24 | 18, 22, 23 | sylancr 588 |
. . . . . . . . . 10
β’ (π΄ β Ο β
((2o βm π΄) Γ (2o βm
{π΄})) β
((2o βm π΄) Γ 2o)) |
25 | | entr 8952 |
. . . . . . . . . 10
β’
(((2o βm (π΄ βͺ {π΄})) β ((2o
βm π΄)
Γ (2o βm {π΄})) β§ ((2o βm
π΄) Γ (2o
βm {π΄}))
β ((2o βm π΄) Γ 2o)) β
(2o βm (π΄ βͺ {π΄})) β ((2o
βm π΄)
Γ 2o)) |
26 | 16, 24, 25 | syl2anc 585 |
. . . . . . . . 9
β’ (π΄ β Ο β
(2o βm (π΄ βͺ {π΄})) β ((2o
βm π΄)
Γ 2o)) |
27 | 5, 26 | eqbrtrid 5144 |
. . . . . . . 8
β’ (π΄ β Ο β
(2o βm suc π΄) β ((2o βm
π΄) Γ
2o)) |
28 | 17, 10 | xpcomen 9013 |
. . . . . . . 8
β’
((2o βm π΄) Γ 2o) β
(2o Γ (2o βm π΄)) |
29 | | entr 8952 |
. . . . . . . 8
β’
(((2o βm suc π΄) β ((2o βm
π΄) Γ 2o)
β§ ((2o βm π΄) Γ 2o) β
(2o Γ (2o βm π΄))) β (2o βm
suc π΄) β
(2o Γ (2o βm π΄))) |
30 | 27, 28, 29 | sylancl 587 |
. . . . . . 7
β’ (π΄ β Ο β
(2o βm suc π΄) β (2o Γ
(2o βm π΄))) |
31 | 10 | enref 8931 |
. . . . . . . . 9
β’
2o β 2o |
32 | | pw2eng 9028 |
. . . . . . . . 9
β’ (π΄ β Ο β π«
π΄ β (2o
βm π΄)) |
33 | | xpen 9090 |
. . . . . . . . 9
β’
((2o β 2o β§ π« π΄ β (2o βm
π΄)) β (2o
Γ π« π΄)
β (2o Γ (2o βm π΄))) |
34 | 31, 32, 33 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β Ο β
(2o Γ π« π΄) β (2o Γ
(2o βm π΄))) |
35 | 34 | ensymd 8951 |
. . . . . . 7
β’ (π΄ β Ο β
(2o Γ (2o βm π΄)) β (2o Γ π«
π΄)) |
36 | | entr 8952 |
. . . . . . 7
β’
(((2o βm suc π΄) β (2o Γ
(2o βm π΄)) β§ (2o Γ
(2o βm π΄)) β (2o Γ π«
π΄)) β (2o
βm suc π΄)
β (2o Γ π« π΄)) |
37 | 30, 35, 36 | syl2anc 585 |
. . . . . 6
β’ (π΄ β Ο β
(2o βm suc π΄) β (2o Γ π«
π΄)) |
38 | | entr 8952 |
. . . . . 6
β’
((π« suc π΄
β (2o βm suc π΄) β§ (2o βm
suc π΄) β
(2o Γ π« π΄)) β π« suc π΄ β (2o Γ π«
π΄)) |
39 | 3, 37, 38 | syl2anc 585 |
. . . . 5
β’ (π΄ β Ο β π«
suc π΄ β
(2o Γ π« π΄)) |
40 | | xp2dju 10120 |
. . . . 5
β’
(2o Γ π« π΄) = (π« π΄ β π« π΄) |
41 | 39, 40 | breqtrdi 5150 |
. . . 4
β’ (π΄ β Ο β π«
suc π΄ β (π«
π΄ β π« π΄)) |
42 | | nnfi 9117 |
. . . . . . . 8
β’ (π΄ β Ο β π΄ β Fin) |
43 | | pwfi 9128 |
. . . . . . . 8
β’ (π΄ β Fin β π«
π΄ β
Fin) |
44 | 42, 43 | sylib 217 |
. . . . . . 7
β’ (π΄ β Ο β π«
π΄ β
Fin) |
45 | | ficardid 9906 |
. . . . . . 7
β’
(π« π΄ β
Fin β (cardβπ« π΄) β π« π΄) |
46 | 44, 45 | syl 17 |
. . . . . 6
β’ (π΄ β Ο β
(cardβπ« π΄)
β π« π΄) |
47 | | djuen 10113 |
. . . . . 6
β’
(((cardβπ« π΄) β π« π΄ β§ (cardβπ« π΄) β π« π΄) β ((cardβπ«
π΄) β
(cardβπ« π΄))
β (π« π΄
β π« π΄)) |
48 | 46, 46, 47 | syl2anc 585 |
. . . . 5
β’ (π΄ β Ο β
((cardβπ« π΄)
β (cardβπ« π΄)) β (π« π΄ β π« π΄)) |
49 | 48 | ensymd 8951 |
. . . 4
β’ (π΄ β Ο β
(π« π΄ β
π« π΄) β
((cardβπ« π΄)
β (cardβπ« π΄))) |
50 | | entr 8952 |
. . . 4
β’
((π« suc π΄
β (π« π΄
β π« π΄) β§
(π« π΄ β
π« π΄) β
((cardβπ« π΄)
β (cardβπ« π΄))) β π« suc π΄ β ((cardβπ« π΄) β (cardβπ«
π΄))) |
51 | 41, 49, 50 | syl2anc 585 |
. . 3
β’ (π΄ β Ο β π«
suc π΄ β
((cardβπ« π΄)
β (cardβπ« π΄))) |
52 | | carden2b 9911 |
. . 3
β’
(π« suc π΄
β ((cardβπ« π΄) β (cardβπ« π΄)) β (cardβπ«
suc π΄) =
(cardβ((cardβπ« π΄) β (cardβπ« π΄)))) |
53 | 51, 52 | syl 17 |
. 2
β’ (π΄ β Ο β
(cardβπ« suc π΄) = (cardβ((cardβπ« π΄) β (cardβπ«
π΄)))) |
54 | | ficardom 9905 |
. . . 4
β’
(π« π΄ β
Fin β (cardβπ« π΄) β Ο) |
55 | 44, 54 | syl 17 |
. . 3
β’ (π΄ β Ο β
(cardβπ« π΄)
β Ο) |
56 | | nnadju 10141 |
. . 3
β’
(((cardβπ« π΄) β Ο β§ (cardβπ«
π΄) β Ο) β
(cardβ((cardβπ« π΄) β (cardβπ« π΄))) = ((cardβπ«
π΄) +o
(cardβπ« π΄))) |
57 | 55, 55, 56 | syl2anc 585 |
. 2
β’ (π΄ β Ο β
(cardβ((cardβπ« π΄) β (cardβπ« π΄))) = ((cardβπ«
π΄) +o
(cardβπ« π΄))) |
58 | 53, 57 | eqtrd 2773 |
1
β’ (π΄ β Ο β
(cardβπ« suc π΄) = ((cardβπ« π΄) +o (cardβπ« π΄))) |