Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . 4
β’ (π = β
β (rec(πΊ, β
)βπ) = (rec(πΊ, β
)ββ
)) |
2 | | suceq 6387 |
. . . . . 6
β’ (π = β
β suc π = suc β
) |
3 | 2 | fveq2d 6850 |
. . . . 5
β’ (π = β
β (rec(πΊ, β
)βsuc π) = (rec(πΊ, β
)βsuc
β
)) |
4 | | fveq2 6846 |
. . . . 5
β’ (π = β
β
(π
1βπ) =
(π
1ββ
)) |
5 | 3, 4 | reseq12d 5942 |
. . . 4
β’ (π = β
β ((rec(πΊ, β
)βsuc π) βΎ
(π
1βπ)) = ((rec(πΊ, β
)βsuc β
) βΎ
(π
1ββ
))) |
6 | 1, 5 | eqeq12d 2749 |
. . 3
β’ (π = β
β ((rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β (rec(πΊ, β
)ββ
) = ((rec(πΊ, β
)βsuc β
)
βΎ (π
1ββ
)))) |
7 | | fveq2 6846 |
. . . 4
β’ (π = π β (rec(πΊ, β
)βπ) = (rec(πΊ, β
)βπ)) |
8 | | suceq 6387 |
. . . . . 6
β’ (π = π β suc π = suc π) |
9 | 8 | fveq2d 6850 |
. . . . 5
β’ (π = π β (rec(πΊ, β
)βsuc π) = (rec(πΊ, β
)βsuc π)) |
10 | | fveq2 6846 |
. . . . 5
β’ (π = π β (π
1βπ) =
(π
1βπ)) |
11 | 9, 10 | reseq12d 5942 |
. . . 4
β’ (π = π β ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) |
12 | 7, 11 | eqeq12d 2749 |
. . 3
β’ (π = π β ((rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))) |
13 | | fveq2 6846 |
. . . 4
β’ (π = suc π β (rec(πΊ, β
)βπ) = (rec(πΊ, β
)βsuc π)) |
14 | | suceq 6387 |
. . . . . 6
β’ (π = suc π β suc π = suc suc π) |
15 | 14 | fveq2d 6850 |
. . . . 5
β’ (π = suc π β (rec(πΊ, β
)βsuc π) = (rec(πΊ, β
)βsuc suc π)) |
16 | | fveq2 6846 |
. . . . 5
β’ (π = suc π β (π
1βπ) =
(π
1βsuc π)) |
17 | 15, 16 | reseq12d 5942 |
. . . 4
β’ (π = suc π β ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) = ((rec(πΊ, β
)βsuc suc π) βΎ (π
1βsuc
π))) |
18 | 13, 17 | eqeq12d 2749 |
. . 3
β’ (π = suc π β ((rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β (rec(πΊ, β
)βsuc π) = ((rec(πΊ, β
)βsuc suc π) βΎ (π
1βsuc
π)))) |
19 | | fveq2 6846 |
. . . 4
β’ (π = π΄ β (rec(πΊ, β
)βπ) = (rec(πΊ, β
)βπ΄)) |
20 | | suceq 6387 |
. . . . . 6
β’ (π = π΄ β suc π = suc π΄) |
21 | 20 | fveq2d 6850 |
. . . . 5
β’ (π = π΄ β (rec(πΊ, β
)βsuc π) = (rec(πΊ, β
)βsuc π΄)) |
22 | | fveq2 6846 |
. . . . 5
β’ (π = π΄ β (π
1βπ) =
(π
1βπ΄)) |
23 | 21, 22 | reseq12d 5942 |
. . . 4
β’ (π = π΄ β ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) = ((rec(πΊ, β
)βsuc π΄) βΎ (π
1βπ΄))) |
24 | 19, 23 | eqeq12d 2749 |
. . 3
β’ (π = π΄ β ((rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β (rec(πΊ, β
)βπ΄) = ((rec(πΊ, β
)βsuc π΄) βΎ (π
1βπ΄)))) |
25 | | res0 5945 |
. . . 4
β’
((rec(πΊ,
β
)βsuc β
) βΎ β
) = β
|
26 | | r10 9712 |
. . . . 5
β’
(π
1ββ
) = β
|
27 | 26 | reseq2i 5938 |
. . . 4
β’
((rec(πΊ,
β
)βsuc β
) βΎ (π
1ββ
)) =
((rec(πΊ, β
)βsuc
β
) βΎ β
) |
28 | | 0ex 5268 |
. . . . 5
β’ β
β V |
29 | 28 | rdg0 8371 |
. . . 4
β’
(rec(πΊ,
β
)ββ
) = β
|
30 | 25, 27, 29 | 3eqtr4ri 2772 |
. . 3
β’
(rec(πΊ,
β
)ββ
) = ((rec(πΊ, β
)βsuc β
) βΎ
(π
1ββ
)) |
31 | | peano2 7831 |
. . . . . . . 8
β’ (π β Ο β suc π β
Ο) |
32 | | ackbij.f |
. . . . . . . . 9
β’ πΉ = (π₯ β (π« Ο β© Fin) β¦
(cardββͺ π¦ β π₯ ({π¦} Γ π« π¦))) |
33 | | ackbij.g |
. . . . . . . . 9
β’ πΊ = (π₯ β V β¦ (π¦ β π« dom π₯ β¦ (πΉβ(π₯ β π¦)))) |
34 | 32, 33 | ackbij2lem2 10184 |
. . . . . . . 8
β’ (suc
π β Ο β
(rec(πΊ, β
)βsuc
π):(π
1βsuc π)β1-1-ontoβ(cardβ(π
1βsuc
π))) |
35 | 31, 34 | syl 17 |
. . . . . . 7
β’ (π β Ο β
(rec(πΊ, β
)βsuc
π):(π
1βsuc π)β1-1-ontoβ(cardβ(π
1βsuc
π))) |
36 | | f1ofn 6789 |
. . . . . . 7
β’
((rec(πΊ,
β
)βsuc π):(π
1βsuc π)β1-1-ontoβ(cardβ(π
1βsuc
π)) β (rec(πΊ, β
)βsuc π) Fn
(π
1βsuc π)) |
37 | 35, 36 | syl 17 |
. . . . . 6
β’ (π β Ο β
(rec(πΊ, β
)βsuc
π) Fn
(π
1βsuc π)) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β (rec(πΊ, β
)βsuc π) Fn
(π
1βsuc π)) |
39 | | peano2 7831 |
. . . . . . . 8
β’ (suc
π β Ο β suc
suc π β
Ο) |
40 | 32, 33 | ackbij2lem2 10184 |
. . . . . . . 8
β’ (suc suc
π β Ο β
(rec(πΊ, β
)βsuc
suc π):(π
1βsuc suc π)β1-1-ontoβ(cardβ(π
1βsuc
suc π))) |
41 | | f1ofn 6789 |
. . . . . . . 8
β’
((rec(πΊ,
β
)βsuc suc π):(π
1βsuc suc π)β1-1-ontoβ(cardβ(π
1βsuc
suc π)) β (rec(πΊ, β
)βsuc suc π) Fn
(π
1βsuc suc π)) |
42 | 31, 39, 40, 41 | 4syl 19 |
. . . . . . 7
β’ (π β Ο β
(rec(πΊ, β
)βsuc
suc π) Fn
(π
1βsuc suc π)) |
43 | | nnon 7812 |
. . . . . . . . 9
β’ (suc
π β Ο β suc
π β
On) |
44 | 31, 43 | syl 17 |
. . . . . . . 8
β’ (π β Ο β suc π β On) |
45 | | r1sssuc 9727 |
. . . . . . . 8
β’ (suc
π β On β
(π
1βsuc π) β (π
1βsuc
suc π)) |
46 | 44, 45 | syl 17 |
. . . . . . 7
β’ (π β Ο β
(π
1βsuc π) β (π
1βsuc
suc π)) |
47 | | fnssres 6628 |
. . . . . . 7
β’
(((rec(πΊ,
β
)βsuc suc π)
Fn (π
1βsuc suc π) β§ (π
1βsuc
π) β
(π
1βsuc suc π)) β ((rec(πΊ, β
)βsuc suc π) βΎ (π
1βsuc
π)) Fn
(π
1βsuc π)) |
48 | 42, 46, 47 | syl2anc 585 |
. . . . . 6
β’ (π β Ο β
((rec(πΊ, β
)βsuc
suc π) βΎ
(π
1βsuc π)) Fn (π
1βsuc π)) |
49 | 48 | adantr 482 |
. . . . 5
β’ ((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β ((rec(πΊ, β
)βsuc suc π) βΎ
(π
1βsuc π)) Fn (π
1βsuc π)) |
50 | | nnon 7812 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β π β On) |
51 | | r1suc 9714 |
. . . . . . . . . . . . . . 15
β’ (π β On β
(π
1βsuc π) = π«
(π
1βπ)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β Ο β
(π
1βsuc π) = π«
(π
1βπ)) |
53 | 52 | eleq2d 2820 |
. . . . . . . . . . . . 13
β’ (π β Ο β (π β
(π
1βsuc π) β π β π«
(π
1βπ))) |
54 | 53 | biimpa 478 |
. . . . . . . . . . . 12
β’ ((π β Ο β§ π β
(π
1βsuc π)) β π β π«
(π
1βπ)) |
55 | 54 | elpwid 4573 |
. . . . . . . . . . 11
β’ ((π β Ο β§ π β
(π
1βsuc π)) β π β (π
1βπ)) |
56 | | resima2 5976 |
. . . . . . . . . . 11
β’ (π β
(π
1βπ) β (((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π) = ((rec(πΊ, β
)βsuc π) β π)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
β’ ((π β Ο β§ π β
(π
1βsuc π)) β (((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π) = ((rec(πΊ, β
)βsuc π) β π)) |
58 | 57 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β Ο β§ π β
(π
1βsuc π)) β (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π)) = (πΉβ((rec(πΊ, β
)βsuc π) β π))) |
59 | | fvex 6859 |
. . . . . . . . . . . . 13
β’
(rec(πΊ,
β
)βsuc π)
β V |
60 | 59 | resex 5989 |
. . . . . . . . . . . 12
β’
((rec(πΊ,
β
)βsuc π)
βΎ (π
1βπ)) β V |
61 | | dmeq 5863 |
. . . . . . . . . . . . . . 15
β’ (π₯ = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β dom π₯ = dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) |
62 | 61 | pweqd 4581 |
. . . . . . . . . . . . . 14
β’ (π₯ = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π« dom π₯ = π« dom ((rec(πΊ, β
)βsuc π) βΎ
(π
1βπ))) |
63 | | imaeq1 6012 |
. . . . . . . . . . . . . . 15
β’ (π₯ = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β (π₯ β π¦) = (((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦)) |
64 | 63 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π₯ = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β (πΉβ(π₯ β π¦)) = (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦))) |
65 | 62, 64 | mpteq12dv 5200 |
. . . . . . . . . . . . 13
β’ (π₯ = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β (π¦ β π« dom π₯ β¦ (πΉβ(π₯ β π¦))) = (π¦ β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦)))) |
66 | 60 | dmex 7852 |
. . . . . . . . . . . . . . 15
β’ dom
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) β V |
67 | 66 | pwex 5339 |
. . . . . . . . . . . . . 14
β’ π«
dom ((rec(πΊ,
β
)βsuc π)
βΎ (π
1βπ)) β V |
68 | 67 | mptex 7177 |
. . . . . . . . . . . . 13
β’ (π¦ β π« dom
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦))) β V |
69 | 65, 33, 68 | fvmpt 6952 |
. . . . . . . . . . . 12
β’
(((rec(πΊ,
β
)βsuc π)
βΎ (π
1βπ)) β V β (πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) = (π¦ β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦)))) |
70 | 60, 69 | ax-mp 5 |
. . . . . . . . . . 11
β’ (πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) = (π¦ β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦))) |
71 | 70 | fveq1i 6847 |
. . . . . . . . . 10
β’ ((πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))βπ) = ((π¦ β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦)))βπ) |
72 | | r1sssuc 9727 |
. . . . . . . . . . . . . . . . 17
β’ (π β On β
(π
1βπ) β (π
1βsuc
π)) |
73 | 50, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β Ο β
(π
1βπ) β (π
1βsuc
π)) |
74 | | fnssres 6628 |
. . . . . . . . . . . . . . . 16
β’
(((rec(πΊ,
β
)βsuc π) Fn
(π
1βsuc π) β§ (π
1βπ) β
(π
1βsuc π)) β ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) Fn
(π
1βπ)) |
75 | 37, 73, 74 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) Fn (π
1βπ)) |
76 | 75 | fndmd 6611 |
. . . . . . . . . . . . . 14
β’ (π β Ο β dom
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) = (π
1βπ)) |
77 | 76 | pweqd 4581 |
. . . . . . . . . . . . 13
β’ (π β Ο β π«
dom ((rec(πΊ,
β
)βsuc π)
βΎ (π
1βπ)) = π«
(π
1βπ)) |
78 | 77 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β Ο β§ π β
(π
1βsuc π)) β π« dom ((rec(πΊ, β
)βsuc π) βΎ
(π
1βπ)) = π«
(π
1βπ)) |
79 | 54, 78 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ ((π β Ο β§ π β
(π
1βsuc π)) β π β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) |
80 | | imaeq2 6013 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦) = (((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π)) |
81 | 80 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π¦ = π β (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦)) = (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π))) |
82 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π¦ β π« dom
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦))) = (π¦ β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦))) |
83 | | fvex 6859 |
. . . . . . . . . . . 12
β’ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π)) β V |
84 | 81, 82, 83 | fvmpt 6952 |
. . . . . . . . . . 11
β’ (π β π« dom
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) β ((π¦ β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦)))βπ) = (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π))) |
85 | 79, 84 | syl 17 |
. . . . . . . . . 10
β’ ((π β Ο β§ π β
(π
1βsuc π)) β ((π¦ β π« dom ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β¦ (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π¦)))βπ) = (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π))) |
86 | 71, 85 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π β Ο β§ π β
(π
1βsuc π)) β ((πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))βπ) = (πΉβ(((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)) β π))) |
87 | | dmeq 5863 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (rec(πΊ, β
)βsuc π) β dom π₯ = dom (rec(πΊ, β
)βsuc π)) |
88 | 87 | pweqd 4581 |
. . . . . . . . . . . . . 14
β’ (π₯ = (rec(πΊ, β
)βsuc π) β π« dom π₯ = π« dom (rec(πΊ, β
)βsuc π)) |
89 | | imaeq1 6012 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (rec(πΊ, β
)βsuc π) β (π₯ β π¦) = ((rec(πΊ, β
)βsuc π) β π¦)) |
90 | 89 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π₯ = (rec(πΊ, β
)βsuc π) β (πΉβ(π₯ β π¦)) = (πΉβ((rec(πΊ, β
)βsuc π) β π¦))) |
91 | 88, 90 | mpteq12dv 5200 |
. . . . . . . . . . . . 13
β’ (π₯ = (rec(πΊ, β
)βsuc π) β (π¦ β π« dom π₯ β¦ (πΉβ(π₯ β π¦))) = (π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦)))) |
92 | 59 | dmex 7852 |
. . . . . . . . . . . . . . 15
β’ dom
(rec(πΊ, β
)βsuc
π) β
V |
93 | 92 | pwex 5339 |
. . . . . . . . . . . . . 14
β’ π«
dom (rec(πΊ,
β
)βsuc π)
β V |
94 | 93 | mptex 7177 |
. . . . . . . . . . . . 13
β’ (π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦))) β V |
95 | 91, 33, 94 | fvmpt 6952 |
. . . . . . . . . . . 12
β’
((rec(πΊ,
β
)βsuc π)
β V β (πΊβ(rec(πΊ, β
)βsuc π)) = (π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦)))) |
96 | 59, 95 | ax-mp 5 |
. . . . . . . . . . 11
β’ (πΊβ(rec(πΊ, β
)βsuc π)) = (π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦))) |
97 | 96 | fveq1i 6847 |
. . . . . . . . . 10
β’ ((πΊβ(rec(πΊ, β
)βsuc π))βπ) = ((π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦)))βπ) |
98 | | r1tr 9720 |
. . . . . . . . . . . . . . 15
β’ Tr
(π
1βsuc π) |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β Ο β Tr
(π
1βsuc π)) |
100 | | dftr4 5233 |
. . . . . . . . . . . . . 14
β’ (Tr
(π
1βsuc π) β (π
1βsuc
π) β π«
(π
1βsuc π)) |
101 | 99, 100 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β Ο β
(π
1βsuc π) β π«
(π
1βsuc π)) |
102 | 101 | sselda 3948 |
. . . . . . . . . . . 12
β’ ((π β Ο β§ π β
(π
1βsuc π)) β π β π«
(π
1βsuc π)) |
103 | | f1odm 6792 |
. . . . . . . . . . . . . . 15
β’
((rec(πΊ,
β
)βsuc π):(π
1βsuc π)β1-1-ontoβ(cardβ(π
1βsuc
π)) β dom (rec(πΊ, β
)βsuc π) =
(π
1βsuc π)) |
104 | 35, 103 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β Ο β dom
(rec(πΊ, β
)βsuc
π) =
(π
1βsuc π)) |
105 | 104 | pweqd 4581 |
. . . . . . . . . . . . 13
β’ (π β Ο β π«
dom (rec(πΊ,
β
)βsuc π) =
π« (π
1βsuc π)) |
106 | 105 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β Ο β§ π β
(π
1βsuc π)) β π« dom (rec(πΊ, β
)βsuc π) = π«
(π
1βsuc π)) |
107 | 102, 106 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ ((π β Ο β§ π β
(π
1βsuc π)) β π β π« dom (rec(πΊ, β
)βsuc π)) |
108 | | imaeq2 6013 |
. . . . . . . . . . . . 13
β’ (π¦ = π β ((rec(πΊ, β
)βsuc π) β π¦) = ((rec(πΊ, β
)βsuc π) β π)) |
109 | 108 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π¦ = π β (πΉβ((rec(πΊ, β
)βsuc π) β π¦)) = (πΉβ((rec(πΊ, β
)βsuc π) β π))) |
110 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦))) = (π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦))) |
111 | | fvex 6859 |
. . . . . . . . . . . 12
β’ (πΉβ((rec(πΊ, β
)βsuc π) β π)) β V |
112 | 109, 110,
111 | fvmpt 6952 |
. . . . . . . . . . 11
β’ (π β π« dom (rec(πΊ, β
)βsuc π) β ((π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦)))βπ) = (πΉβ((rec(πΊ, β
)βsuc π) β π))) |
113 | 107, 112 | syl 17 |
. . . . . . . . . 10
β’ ((π β Ο β§ π β
(π
1βsuc π)) β ((π¦ β π« dom (rec(πΊ, β
)βsuc π) β¦ (πΉβ((rec(πΊ, β
)βsuc π) β π¦)))βπ) = (πΉβ((rec(πΊ, β
)βsuc π) β π))) |
114 | 97, 113 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π β Ο β§ π β
(π
1βsuc π)) β ((πΊβ(rec(πΊ, β
)βsuc π))βπ) = (πΉβ((rec(πΊ, β
)βsuc π) β π))) |
115 | 58, 86, 114 | 3eqtr4d 2783 |
. . . . . . . 8
β’ ((π β Ο β§ π β
(π
1βsuc π)) β ((πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))βπ) = ((πΊβ(rec(πΊ, β
)βsuc π))βπ)) |
116 | 115 | adantlr 714 |
. . . . . . 7
β’ (((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β§ π β (π
1βsuc
π)) β ((πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))βπ) = ((πΊβ(rec(πΊ, β
)βsuc π))βπ)) |
117 | | fveq2 6846 |
. . . . . . . . 9
β’
((rec(πΊ,
β
)βπ) =
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) β (πΊβ(rec(πΊ, β
)βπ)) = (πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))) |
118 | 117 | fveq1d 6848 |
. . . . . . . 8
β’
((rec(πΊ,
β
)βπ) =
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) β ((πΊβ(rec(πΊ, β
)βπ))βπ) = ((πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))βπ)) |
119 | 118 | ad2antlr 726 |
. . . . . . 7
β’ (((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β§ π β (π
1βsuc
π)) β ((πΊβ(rec(πΊ, β
)βπ))βπ) = ((πΊβ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ)))βπ)) |
120 | | rdgsuc 8374 |
. . . . . . . . . 10
β’ (suc
π β On β
(rec(πΊ, β
)βsuc
suc π) = (πΊβ(rec(πΊ, β
)βsuc π))) |
121 | 44, 120 | syl 17 |
. . . . . . . . 9
β’ (π β Ο β
(rec(πΊ, β
)βsuc
suc π) = (πΊβ(rec(πΊ, β
)βsuc π))) |
122 | 121 | fveq1d 6848 |
. . . . . . . 8
β’ (π β Ο β
((rec(πΊ, β
)βsuc
suc π)βπ) = ((πΊβ(rec(πΊ, β
)βsuc π))βπ)) |
123 | 122 | ad2antrr 725 |
. . . . . . 7
β’ (((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β§ π β (π
1βsuc
π)) β ((rec(πΊ, β
)βsuc suc π)βπ) = ((πΊβ(rec(πΊ, β
)βsuc π))βπ)) |
124 | 116, 119,
123 | 3eqtr4rd 2784 |
. . . . . 6
β’ (((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β§ π β (π
1βsuc
π)) β ((rec(πΊ, β
)βsuc suc π)βπ) = ((πΊβ(rec(πΊ, β
)βπ))βπ)) |
125 | | fvres 6865 |
. . . . . . 7
β’ (π β
(π
1βsuc π) β (((rec(πΊ, β
)βsuc suc π) βΎ (π
1βsuc
π))βπ) = ((rec(πΊ, β
)βsuc suc π)βπ)) |
126 | 125 | adantl 483 |
. . . . . 6
β’ (((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β§ π β (π
1βsuc
π)) β (((rec(πΊ, β
)βsuc suc π) βΎ
(π
1βsuc π))βπ) = ((rec(πΊ, β
)βsuc suc π)βπ)) |
127 | | rdgsuc 8374 |
. . . . . . . . 9
β’ (π β On β (rec(πΊ, β
)βsuc π) = (πΊβ(rec(πΊ, β
)βπ))) |
128 | 50, 127 | syl 17 |
. . . . . . . 8
β’ (π β Ο β
(rec(πΊ, β
)βsuc
π) = (πΊβ(rec(πΊ, β
)βπ))) |
129 | 128 | fveq1d 6848 |
. . . . . . 7
β’ (π β Ο β
((rec(πΊ, β
)βsuc
π)βπ) = ((πΊβ(rec(πΊ, β
)βπ))βπ)) |
130 | 129 | ad2antrr 725 |
. . . . . 6
β’ (((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β§ π β (π
1βsuc
π)) β ((rec(πΊ, β
)βsuc π)βπ) = ((πΊβ(rec(πΊ, β
)βπ))βπ)) |
131 | 124, 126,
130 | 3eqtr4rd 2784 |
. . . . 5
β’ (((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β§ π β (π
1βsuc
π)) β ((rec(πΊ, β
)βsuc π)βπ) = (((rec(πΊ, β
)βsuc suc π) βΎ (π
1βsuc
π))βπ)) |
132 | 38, 49, 131 | eqfnfvd 6989 |
. . . 4
β’ ((π β Ο β§ (rec(πΊ, β
)βπ) = ((rec(πΊ, β
)βsuc π) βΎ (π
1βπ))) β (rec(πΊ, β
)βsuc π) = ((rec(πΊ, β
)βsuc suc π) βΎ (π
1βsuc
π))) |
133 | 132 | ex 414 |
. . 3
β’ (π β Ο β
((rec(πΊ,
β
)βπ) =
((rec(πΊ, β
)βsuc
π) βΎ
(π
1βπ)) β (rec(πΊ, β
)βsuc π) = ((rec(πΊ, β
)βsuc suc π) βΎ (π
1βsuc
π)))) |
134 | 6, 12, 18, 24, 30, 133 | finds 7839 |
. 2
β’ (π΄ β Ο β
(rec(πΊ,
β
)βπ΄) =
((rec(πΊ, β
)βsuc
π΄) βΎ
(π
1βπ΄))) |
135 | | resss 5966 |
. 2
β’
((rec(πΊ,
β
)βsuc π΄)
βΎ (π
1βπ΄)) β (rec(πΊ, β
)βsuc π΄) |
136 | 134, 135 | eqsstrdi 4002 |
1
β’ (π΄ β Ο β
(rec(πΊ,
β
)βπ΄) β
(rec(πΊ, β
)βsuc
π΄)) |