Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (rec(πΊ, β
)βπ) = (rec(πΊ, β
)βπ)) |
2 | | fvex 6856 |
. . . . . 6
β’
(rec(πΊ,
β
)βπ) β
V |
3 | 1, 2 | f1iun 7877 |
. . . . 5
β’
(βπ β
Ο ((rec(πΊ,
β
)βπ):(π
1βπ)β1-1βΟ β§ βπ β Ο ((rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ) β¨ (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ))) β βͺ π β Ο (rec(πΊ, β
)βπ):βͺ π β Ο
(π
1βπ)β1-1βΟ) |
4 | | ackbij.f |
. . . . . . . . 9
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
5 | | ackbij.g |
. . . . . . . . 9
β’ πΊ = (π₯ β V β¦ (π¦ β π« dom π₯ β¦ (πΉβ(π₯ β π¦)))) |
6 | 4, 5 | ackbij2lem2 10181 |
. . . . . . . 8
β’ (π β Ο β
(rec(πΊ,
β
)βπ):(π
1βπ)β1-1-ontoβ(cardβ(π
1βπ))) |
7 | | f1of1 6784 |
. . . . . . . 8
β’
((rec(πΊ,
β
)βπ):(π
1βπ)β1-1-ontoβ(cardβ(π
1βπ)) β (rec(πΊ, β
)βπ):(π
1βπ)β1-1β(cardβ(π
1βπ))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’ (π β Ο β
(rec(πΊ,
β
)βπ):(π
1βπ)β1-1β(cardβ(π
1βπ))) |
9 | | ordom 7813 |
. . . . . . . 8
β’ Ord
Ο |
10 | | r1fin 9714 |
. . . . . . . . 9
β’ (π β Ο β
(π
1βπ) β Fin) |
11 | | ficardom 9902 |
. . . . . . . . 9
β’
((π
1βπ) β Fin β
(cardβ(π
1βπ)) β Ο) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
β’ (π β Ο β
(cardβ(π
1βπ)) β Ο) |
13 | | ordelss 6334 |
. . . . . . . 8
β’ ((Ord
Ο β§ (cardβ(π
1βπ)) β Ο) β
(cardβ(π
1βπ)) β Ο) |
14 | 9, 12, 13 | sylancr 588 |
. . . . . . 7
β’ (π β Ο β
(cardβ(π
1βπ)) β Ο) |
15 | | f1ss 6745 |
. . . . . . 7
β’
(((rec(πΊ,
β
)βπ):(π
1βπ)β1-1β(cardβ(π
1βπ)) β§
(cardβ(π
1βπ)) β Ο) β (rec(πΊ, β
)βπ):(π
1βπ)β1-1βΟ) |
16 | 8, 14, 15 | syl2anc 585 |
. . . . . 6
β’ (π β Ο β
(rec(πΊ,
β
)βπ):(π
1βπ)β1-1βΟ) |
17 | | nnord 7811 |
. . . . . . . . 9
β’ (π β Ο β Ord π) |
18 | | nnord 7811 |
. . . . . . . . 9
β’ (π β Ο β Ord π) |
19 | | ordtri2or2 6417 |
. . . . . . . . 9
β’ ((Ord
π β§ Ord π) β (π β π β¨ π β π)) |
20 | 17, 18, 19 | syl2an 597 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β (π β π β¨ π β π)) |
21 | 4, 5 | ackbij2lem4 10183 |
. . . . . . . . . . 11
β’ (((π β Ο β§ π β Ο) β§ π β π) β (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ)) |
22 | 21 | ex 414 |
. . . . . . . . . 10
β’ ((π β Ο β§ π β Ο) β (π β π β (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ))) |
23 | 22 | ancoms 460 |
. . . . . . . . 9
β’ ((π β Ο β§ π β Ο) β (π β π β (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ))) |
24 | 4, 5 | ackbij2lem4 10183 |
. . . . . . . . . 10
β’ (((π β Ο β§ π β Ο) β§ π β π) β (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ)) |
25 | 24 | ex 414 |
. . . . . . . . 9
β’ ((π β Ο β§ π β Ο) β (π β π β (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ))) |
26 | 23, 25 | orim12d 964 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β ((π β π β¨ π β π) β ((rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ) β¨ (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ)))) |
27 | 20, 26 | mpd 15 |
. . . . . . 7
β’ ((π β Ο β§ π β Ο) β
((rec(πΊ,
β
)βπ) β
(rec(πΊ,
β
)βπ) β¨
(rec(πΊ,
β
)βπ) β
(rec(πΊ,
β
)βπ))) |
28 | 27 | ralrimiva 3140 |
. . . . . 6
β’ (π β Ο β
βπ β Ο
((rec(πΊ,
β
)βπ) β
(rec(πΊ,
β
)βπ) β¨
(rec(πΊ,
β
)βπ) β
(rec(πΊ,
β
)βπ))) |
29 | 16, 28 | jca 513 |
. . . . 5
β’ (π β Ο β
((rec(πΊ,
β
)βπ):(π
1βπ)β1-1βΟ β§ βπ β Ο ((rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ) β¨ (rec(πΊ, β
)βπ) β (rec(πΊ, β
)βπ)))) |
30 | 3, 29 | mprg 3067 |
. . . 4
β’ βͺ π β Ο (rec(πΊ, β
)βπ):βͺ π β Ο
(π
1βπ)β1-1βΟ |
31 | | rdgfun 8363 |
. . . . . 6
β’ Fun
rec(πΊ,
β
) |
32 | | funiunfv 7196 |
. . . . . . 7
β’ (Fun
rec(πΊ, β
) β
βͺ π β Ο (rec(πΊ, β
)βπ) = βͺ (rec(πΊ, β
) β
Ο)) |
33 | 32 | eqcomd 2739 |
. . . . . 6
β’ (Fun
rec(πΊ, β
) β
βͺ (rec(πΊ, β
) β Ο) = βͺ π β Ο (rec(πΊ, β
)βπ)) |
34 | | f1eq1 6734 |
. . . . . 6
β’ (βͺ (rec(πΊ, β
) β Ο) = βͺ π β Ο (rec(πΊ, β
)βπ) β (βͺ
(rec(πΊ, β
) β
Ο):βͺ (π
1 β
Ο)β1-1βΟ β
βͺ π β Ο (rec(πΊ, β
)βπ):βͺ
(π
1 β Ο)β1-1βΟ)) |
35 | 31, 33, 34 | mp2b 10 |
. . . . 5
β’ (βͺ (rec(πΊ, β
) β Ο):βͺ (π
1 β Ο)β1-1βΟ β βͺ π β Ο (rec(πΊ, β
)βπ):βͺ
(π
1 β Ο)β1-1βΟ) |
36 | | r1funlim 9707 |
. . . . . . 7
β’ (Fun
π
1 β§ Lim dom π
1) |
37 | 36 | simpli 485 |
. . . . . 6
β’ Fun
π
1 |
38 | | funiunfv 7196 |
. . . . . 6
β’ (Fun
π
1 β βͺ π β Ο
(π
1βπ) = βͺ
(π
1 β Ο)) |
39 | | f1eq2 6735 |
. . . . . 6
β’ (βͺ π β Ο
(π
1βπ) = βͺ
(π
1 β Ο) β (βͺ π β Ο (rec(πΊ, β
)βπ):βͺ π β Ο
(π
1βπ)β1-1βΟ β βͺ π β Ο (rec(πΊ, β
)βπ):βͺ
(π
1 β Ο)β1-1βΟ)) |
40 | 37, 38, 39 | mp2b 10 |
. . . . 5
β’ (βͺ π β Ο (rec(πΊ, β
)βπ):βͺ π β Ο
(π
1βπ)β1-1βΟ β βͺ π β Ο (rec(πΊ, β
)βπ):βͺ
(π
1 β Ο)β1-1βΟ) |
41 | 35, 40 | bitr4i 278 |
. . . 4
β’ (βͺ (rec(πΊ, β
) β Ο):βͺ (π
1 β Ο)β1-1βΟ β βͺ π β Ο (rec(πΊ, β
)βπ):βͺ π β Ο
(π
1βπ)β1-1βΟ) |
42 | 30, 41 | mpbir 230 |
. . 3
β’ βͺ (rec(πΊ, β
) β Ο):βͺ (π
1 β Ο)β1-1βΟ |
43 | | rnuni 6102 |
. . . 4
β’ ran βͺ (rec(πΊ, β
) β Ο) = βͺ π β (rec(πΊ, β
) β Ο)ran π |
44 | | eliun 4959 |
. . . . . 6
β’ (π β βͺ π β (rec(πΊ, β
) β Ο)ran π β βπ β (rec(πΊ, β
) β Ο)π β ran π) |
45 | | df-rex 3071 |
. . . . . 6
β’
(βπ β
(rec(πΊ, β
) β
Ο)π β ran π β βπ(π β (rec(πΊ, β
) β Ο) β§ π β ran π)) |
46 | | funfn 6532 |
. . . . . . . . . . . 12
β’ (Fun
rec(πΊ, β
) β
rec(πΊ, β
) Fn dom
rec(πΊ,
β
)) |
47 | 31, 46 | mpbi 229 |
. . . . . . . . . . 11
β’ rec(πΊ, β
) Fn dom rec(πΊ, β
) |
48 | | rdgdmlim 8364 |
. . . . . . . . . . . 12
β’ Lim dom
rec(πΊ,
β
) |
49 | | limomss 7808 |
. . . . . . . . . . . 12
β’ (Lim dom
rec(πΊ, β
) β
Ο β dom rec(πΊ,
β
)) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . 11
β’ Ο
β dom rec(πΊ,
β
) |
51 | | fvelimab 6915 |
. . . . . . . . . . 11
β’
((rec(πΊ, β
) Fn
dom rec(πΊ, β
) β§
Ο β dom rec(πΊ,
β
)) β (π β
(rec(πΊ, β
) β
Ο) β βπ
β Ο (rec(πΊ,
β
)βπ) = π)) |
52 | 47, 50, 51 | mp2an 691 |
. . . . . . . . . 10
β’ (π β (rec(πΊ, β
) β Ο) β
βπ β Ο
(rec(πΊ,
β
)βπ) = π) |
53 | 4, 5 | ackbij2lem2 10181 |
. . . . . . . . . . . . . 14
β’ (π β Ο β
(rec(πΊ,
β
)βπ):(π
1βπ)β1-1-ontoβ(cardβ(π
1βπ))) |
54 | | f1ofo 6792 |
. . . . . . . . . . . . . 14
β’
((rec(πΊ,
β
)βπ):(π
1βπ)β1-1-ontoβ(cardβ(π
1βπ)) β (rec(πΊ, β
)βπ):(π
1βπ)βontoβ(cardβ(π
1βπ))) |
55 | | forn 6760 |
. . . . . . . . . . . . . 14
β’
((rec(πΊ,
β
)βπ):(π
1βπ)βontoβ(cardβ(π
1βπ)) β ran (rec(πΊ, β
)βπ) =
(cardβ(π
1βπ))) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β Ο β ran
(rec(πΊ,
β
)βπ) =
(cardβ(π
1βπ))) |
57 | | r1fin 9714 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β
(π
1βπ) β Fin) |
58 | | ficardom 9902 |
. . . . . . . . . . . . . . 15
β’
((π
1βπ) β Fin β
(cardβ(π
1βπ)) β Ο) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β Ο β
(cardβ(π
1βπ)) β Ο) |
60 | | ordelss 6334 |
. . . . . . . . . . . . . 14
β’ ((Ord
Ο β§ (cardβ(π
1βπ)) β Ο) β
(cardβ(π
1βπ)) β Ο) |
61 | 9, 59, 60 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π β Ο β
(cardβ(π
1βπ)) β Ο) |
62 | 56, 61 | eqsstrd 3983 |
. . . . . . . . . . . 12
β’ (π β Ο β ran
(rec(πΊ,
β
)βπ) β
Ο) |
63 | | rneq 5892 |
. . . . . . . . . . . . 13
β’
((rec(πΊ,
β
)βπ) = π β ran (rec(πΊ, β
)βπ) = ran π) |
64 | 63 | sseq1d 3976 |
. . . . . . . . . . . 12
β’
((rec(πΊ,
β
)βπ) = π β (ran (rec(πΊ, β
)βπ) β Ο β ran
π β
Ο)) |
65 | 62, 64 | syl5ibcom 244 |
. . . . . . . . . . 11
β’ (π β Ο β
((rec(πΊ,
β
)βπ) = π β ran π β Ο)) |
66 | 65 | rexlimiv 3142 |
. . . . . . . . . 10
β’
(βπ β
Ο (rec(πΊ,
β
)βπ) = π β ran π β Ο) |
67 | 52, 66 | sylbi 216 |
. . . . . . . . 9
β’ (π β (rec(πΊ, β
) β Ο) β ran π β
Ο) |
68 | 67 | sselda 3945 |
. . . . . . . 8
β’ ((π β (rec(πΊ, β
) β Ο) β§ π β ran π) β π β Ο) |
69 | 68 | exlimiv 1934 |
. . . . . . 7
β’
(βπ(π β (rec(πΊ, β
) β Ο) β§ π β ran π) β π β Ο) |
70 | | peano2 7828 |
. . . . . . . . 9
β’ (π β Ο β suc π β
Ο) |
71 | | fnfvima 7184 |
. . . . . . . . 9
β’
((rec(πΊ, β
) Fn
dom rec(πΊ, β
) β§
Ο β dom rec(πΊ,
β
) β§ suc π β
Ο) β (rec(πΊ,
β
)βsuc π)
β (rec(πΊ, β
)
β Ο)) |
72 | 47, 50, 70, 71 | mp3an12i 1466 |
. . . . . . . 8
β’ (π β Ο β
(rec(πΊ, β
)βsuc
π) β (rec(πΊ, β
) β
Ο)) |
73 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
74 | | cardnn 9904 |
. . . . . . . . . . . 12
β’ (suc
π β Ο β
(cardβsuc π) = suc
π) |
75 | | fvex 6856 |
. . . . . . . . . . . . . 14
β’
(π
1βsuc π) β V |
76 | 36 | simpri 487 |
. . . . . . . . . . . . . . . . 17
β’ Lim dom
π
1 |
77 | | limomss 7808 |
. . . . . . . . . . . . . . . . 17
β’ (Lim dom
π
1 β Ο β dom
π
1) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ Ο
β dom π
1 |
79 | 78 | sseli 3941 |
. . . . . . . . . . . . . . 15
β’ (suc
π β Ο β suc
π β dom
π
1) |
80 | | onssr1 9772 |
. . . . . . . . . . . . . . 15
β’ (suc
π β dom
π
1 β suc π β (π
1βsuc
π)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . 14
β’ (suc
π β Ο β suc
π β
(π
1βsuc π)) |
82 | | ssdomg 8943 |
. . . . . . . . . . . . . 14
β’
((π
1βsuc π) β V β (suc π β (π
1βsuc
π) β suc π βΌ
(π
1βsuc π))) |
83 | 75, 81, 82 | mpsyl 68 |
. . . . . . . . . . . . 13
β’ (suc
π β Ο β suc
π βΌ
(π
1βsuc π)) |
84 | | nnon 7809 |
. . . . . . . . . . . . . . 15
β’ (suc
π β Ο β suc
π β
On) |
85 | | onenon 9890 |
. . . . . . . . . . . . . . 15
β’ (suc
π β On β suc
π β dom
card) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . 14
β’ (suc
π β Ο β suc
π β dom
card) |
87 | | r1fin 9714 |
. . . . . . . . . . . . . . 15
β’ (suc
π β Ο β
(π
1βsuc π) β Fin) |
88 | | finnum 9889 |
. . . . . . . . . . . . . . 15
β’
((π
1βsuc π) β Fin β
(π
1βsuc π) β dom card) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . 14
β’ (suc
π β Ο β
(π
1βsuc π) β dom card) |
90 | | carddom2 9918 |
. . . . . . . . . . . . . 14
β’ ((suc
π β dom card β§
(π
1βsuc π) β dom card) β ((cardβsuc
π) β
(cardβ(π
1βsuc π)) β suc π βΌ (π
1βsuc
π))) |
91 | 86, 89, 90 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (suc
π β Ο β
((cardβsuc π) β
(cardβ(π
1βsuc π)) β suc π βΌ (π
1βsuc
π))) |
92 | 83, 91 | mpbird 257 |
. . . . . . . . . . . 12
β’ (suc
π β Ο β
(cardβsuc π) β
(cardβ(π
1βsuc π))) |
93 | 74, 92 | eqsstrrd 3984 |
. . . . . . . . . . 11
β’ (suc
π β Ο β suc
π β
(cardβ(π
1βsuc π))) |
94 | 70, 93 | syl 17 |
. . . . . . . . . 10
β’ (π β Ο β suc π β
(cardβ(π
1βsuc π))) |
95 | | sucssel 6413 |
. . . . . . . . . 10
β’ (π β V β (suc π β
(cardβ(π
1βsuc π)) β π β
(cardβ(π
1βsuc π)))) |
96 | 73, 94, 95 | mpsyl 68 |
. . . . . . . . 9
β’ (π β Ο β π β
(cardβ(π
1βsuc π))) |
97 | 4, 5 | ackbij2lem2 10181 |
. . . . . . . . . 10
β’ (suc
π β Ο β
(rec(πΊ, β
)βsuc
π):(π
1βsuc π)β1-1-ontoβ(cardβ(π
1βsuc
π))) |
98 | | f1ofo 6792 |
. . . . . . . . . 10
β’
((rec(πΊ,
β
)βsuc π):(π
1βsuc π)β1-1-ontoβ(cardβ(π
1βsuc
π)) β (rec(πΊ, β
)βsuc π):(π
1βsuc π)βontoβ(cardβ(π
1βsuc
π))) |
99 | | forn 6760 |
. . . . . . . . . 10
β’
((rec(πΊ,
β
)βsuc π):(π
1βsuc π)βontoβ(cardβ(π
1βsuc
π)) β ran (rec(πΊ, β
)βsuc π) =
(cardβ(π
1βsuc π))) |
100 | 70, 97, 98, 99 | 4syl 19 |
. . . . . . . . 9
β’ (π β Ο β ran
(rec(πΊ, β
)βsuc
π) =
(cardβ(π
1βsuc π))) |
101 | 96, 100 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β Ο β π β ran (rec(πΊ, β
)βsuc π)) |
102 | | fvex 6856 |
. . . . . . . . 9
β’
(rec(πΊ,
β
)βsuc π)
β V |
103 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = (rec(πΊ, β
)βsuc π) β (π β (rec(πΊ, β
) β Ο) β
(rec(πΊ, β
)βsuc
π) β (rec(πΊ, β
) β
Ο))) |
104 | | rneq 5892 |
. . . . . . . . . . 11
β’ (π = (rec(πΊ, β
)βsuc π) β ran π = ran (rec(πΊ, β
)βsuc π)) |
105 | 104 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π = (rec(πΊ, β
)βsuc π) β (π β ran π β π β ran (rec(πΊ, β
)βsuc π))) |
106 | 103, 105 | anbi12d 632 |
. . . . . . . . 9
β’ (π = (rec(πΊ, β
)βsuc π) β ((π β (rec(πΊ, β
) β Ο) β§ π β ran π) β ((rec(πΊ, β
)βsuc π) β (rec(πΊ, β
) β Ο) β§ π β ran (rec(πΊ, β
)βsuc π)))) |
107 | 102, 106 | spcev 3564 |
. . . . . . . 8
β’
(((rec(πΊ,
β
)βsuc π)
β (rec(πΊ, β
)
β Ο) β§ π
β ran (rec(πΊ,
β
)βsuc π))
β βπ(π β (rec(πΊ, β
) β Ο) β§ π β ran π)) |
108 | 72, 101, 107 | syl2anc 585 |
. . . . . . 7
β’ (π β Ο β
βπ(π β (rec(πΊ, β
) β Ο) β§ π β ran π)) |
109 | 69, 108 | impbii 208 |
. . . . . 6
β’
(βπ(π β (rec(πΊ, β
) β Ο) β§ π β ran π) β π β Ο) |
110 | 44, 45, 109 | 3bitri 297 |
. . . . 5
β’ (π β βͺ π β (rec(πΊ, β
) β Ο)ran π β π β Ο) |
111 | 110 | eqriv 2730 |
. . . 4
β’ βͺ π β (rec(πΊ, β
) β Ο)ran π = Ο |
112 | 43, 111 | eqtri 2761 |
. . 3
β’ ran βͺ (rec(πΊ, β
) β Ο) =
Ο |
113 | | dff1o5 6794 |
. . 3
β’ (βͺ (rec(πΊ, β
) β Ο):βͺ (π
1 β Ο)β1-1-ontoβΟ β (βͺ
(rec(πΊ, β
) β
Ο):βͺ (π
1 β
Ο)β1-1βΟ β§ ran
βͺ (rec(πΊ, β
) β Ο) =
Ο)) |
114 | 42, 112, 113 | mpbir2an 710 |
. 2
β’ βͺ (rec(πΊ, β
) β Ο):βͺ (π
1 β Ο)β1-1-ontoβΟ |
115 | | ackbij.h |
. . 3
β’ π» = βͺ
(rec(πΊ, β
) β
Ο) |
116 | | f1oeq1 6773 |
. . 3
β’ (π» = βͺ
(rec(πΊ, β
) β
Ο) β (π»:βͺ (π
1 β Ο)β1-1-ontoβΟ β βͺ
(rec(πΊ, β
) β
Ο):βͺ (π
1 β
Ο)β1-1-ontoβΟ)) |
117 | 115, 116 | ax-mp 5 |
. 2
β’ (π»:βͺ
(π
1 β Ο)β1-1-ontoβΟ β βͺ
(rec(πΊ, β
) β
Ο):βͺ (π
1 β
Ο)β1-1-ontoβΟ) |
118 | 114, 117 | mpbir 230 |
1
β’ π»:βͺ
(π
1 β Ο)β1-1-ontoβΟ |