Step |
Hyp |
Ref |
Expression |
1 |
|
ackbij.f |
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) ) |
2 |
|
ackbij.g |
|- G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) ) |
3 |
|
fveq2 |
|- ( a = (/) -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` (/) ) ) |
4 |
|
suceq |
|- ( a = (/) -> suc a = suc (/) ) |
5 |
4
|
fveq2d |
|- ( a = (/) -> ( rec ( G , (/) ) ` suc a ) = ( rec ( G , (/) ) ` suc (/) ) ) |
6 |
|
fveq2 |
|- ( a = (/) -> ( R1 ` a ) = ( R1 ` (/) ) ) |
7 |
5 6
|
reseq12d |
|- ( a = (/) -> ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) = ( ( rec ( G , (/) ) ` suc (/) ) |` ( R1 ` (/) ) ) ) |
8 |
3 7
|
eqeq12d |
|- ( a = (/) -> ( ( rec ( G , (/) ) ` a ) = ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` (/) ) = ( ( rec ( G , (/) ) ` suc (/) ) |` ( R1 ` (/) ) ) ) ) |
9 |
|
fveq2 |
|- ( a = b -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` b ) ) |
10 |
|
suceq |
|- ( a = b -> suc a = suc b ) |
11 |
10
|
fveq2d |
|- ( a = b -> ( rec ( G , (/) ) ` suc a ) = ( rec ( G , (/) ) ` suc b ) ) |
12 |
|
fveq2 |
|- ( a = b -> ( R1 ` a ) = ( R1 ` b ) ) |
13 |
11 12
|
reseq12d |
|- ( a = b -> ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) |
14 |
9 13
|
eqeq12d |
|- ( a = b -> ( ( rec ( G , (/) ) ` a ) = ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ) |
15 |
|
fveq2 |
|- ( a = suc b -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` suc b ) ) |
16 |
|
suceq |
|- ( a = suc b -> suc a = suc suc b ) |
17 |
16
|
fveq2d |
|- ( a = suc b -> ( rec ( G , (/) ) ` suc a ) = ( rec ( G , (/) ) ` suc suc b ) ) |
18 |
|
fveq2 |
|- ( a = suc b -> ( R1 ` a ) = ( R1 ` suc b ) ) |
19 |
17 18
|
reseq12d |
|- ( a = suc b -> ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) = ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) ) |
20 |
15 19
|
eqeq12d |
|- ( a = suc b -> ( ( rec ( G , (/) ) ` a ) = ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` suc b ) = ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) ) ) |
21 |
|
fveq2 |
|- ( a = A -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` A ) ) |
22 |
|
suceq |
|- ( a = A -> suc a = suc A ) |
23 |
22
|
fveq2d |
|- ( a = A -> ( rec ( G , (/) ) ` suc a ) = ( rec ( G , (/) ) ` suc A ) ) |
24 |
|
fveq2 |
|- ( a = A -> ( R1 ` a ) = ( R1 ` A ) ) |
25 |
23 24
|
reseq12d |
|- ( a = A -> ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) = ( ( rec ( G , (/) ) ` suc A ) |` ( R1 ` A ) ) ) |
26 |
21 25
|
eqeq12d |
|- ( a = A -> ( ( rec ( G , (/) ) ` a ) = ( ( rec ( G , (/) ) ` suc a ) |` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` A ) = ( ( rec ( G , (/) ) ` suc A ) |` ( R1 ` A ) ) ) ) |
27 |
|
res0 |
|- ( ( rec ( G , (/) ) ` suc (/) ) |` (/) ) = (/) |
28 |
|
r10 |
|- ( R1 ` (/) ) = (/) |
29 |
28
|
reseq2i |
|- ( ( rec ( G , (/) ) ` suc (/) ) |` ( R1 ` (/) ) ) = ( ( rec ( G , (/) ) ` suc (/) ) |` (/) ) |
30 |
|
0ex |
|- (/) e. _V |
31 |
30
|
rdg0 |
|- ( rec ( G , (/) ) ` (/) ) = (/) |
32 |
27 29 31
|
3eqtr4ri |
|- ( rec ( G , (/) ) ` (/) ) = ( ( rec ( G , (/) ) ` suc (/) ) |` ( R1 ` (/) ) ) |
33 |
|
peano2 |
|- ( b e. _om -> suc b e. _om ) |
34 |
1 2
|
ackbij2lem2 |
|- ( suc b e. _om -> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) ) |
35 |
33 34
|
syl |
|- ( b e. _om -> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) ) |
36 |
|
f1ofn |
|- ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) -> ( rec ( G , (/) ) ` suc b ) Fn ( R1 ` suc b ) ) |
37 |
35 36
|
syl |
|- ( b e. _om -> ( rec ( G , (/) ) ` suc b ) Fn ( R1 ` suc b ) ) |
38 |
37
|
adantr |
|- ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) -> ( rec ( G , (/) ) ` suc b ) Fn ( R1 ` suc b ) ) |
39 |
|
peano2 |
|- ( suc b e. _om -> suc suc b e. _om ) |
40 |
1 2
|
ackbij2lem2 |
|- ( suc suc b e. _om -> ( rec ( G , (/) ) ` suc suc b ) : ( R1 ` suc suc b ) -1-1-onto-> ( card ` ( R1 ` suc suc b ) ) ) |
41 |
|
f1ofn |
|- ( ( rec ( G , (/) ) ` suc suc b ) : ( R1 ` suc suc b ) -1-1-onto-> ( card ` ( R1 ` suc suc b ) ) -> ( rec ( G , (/) ) ` suc suc b ) Fn ( R1 ` suc suc b ) ) |
42 |
33 39 40 41
|
4syl |
|- ( b e. _om -> ( rec ( G , (/) ) ` suc suc b ) Fn ( R1 ` suc suc b ) ) |
43 |
|
nnon |
|- ( suc b e. _om -> suc b e. On ) |
44 |
33 43
|
syl |
|- ( b e. _om -> suc b e. On ) |
45 |
|
r1sssuc |
|- ( suc b e. On -> ( R1 ` suc b ) C_ ( R1 ` suc suc b ) ) |
46 |
44 45
|
syl |
|- ( b e. _om -> ( R1 ` suc b ) C_ ( R1 ` suc suc b ) ) |
47 |
|
fnssres |
|- ( ( ( rec ( G , (/) ) ` suc suc b ) Fn ( R1 ` suc suc b ) /\ ( R1 ` suc b ) C_ ( R1 ` suc suc b ) ) -> ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) Fn ( R1 ` suc b ) ) |
48 |
42 46 47
|
syl2anc |
|- ( b e. _om -> ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) Fn ( R1 ` suc b ) ) |
49 |
48
|
adantr |
|- ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) -> ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) Fn ( R1 ` suc b ) ) |
50 |
|
nnon |
|- ( b e. _om -> b e. On ) |
51 |
|
r1suc |
|- ( b e. On -> ( R1 ` suc b ) = ~P ( R1 ` b ) ) |
52 |
50 51
|
syl |
|- ( b e. _om -> ( R1 ` suc b ) = ~P ( R1 ` b ) ) |
53 |
52
|
eleq2d |
|- ( b e. _om -> ( c e. ( R1 ` suc b ) <-> c e. ~P ( R1 ` b ) ) ) |
54 |
53
|
biimpa |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> c e. ~P ( R1 ` b ) ) |
55 |
54
|
elpwid |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> c C_ ( R1 ` b ) ) |
56 |
|
resima2 |
|- ( c C_ ( R1 ` b ) -> ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) = ( ( rec ( G , (/) ) ` suc b ) " c ) ) |
57 |
55 56
|
syl |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) = ( ( rec ( G , (/) ) ` suc b ) " c ) ) |
58 |
57
|
fveq2d |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) ) = ( F ` ( ( rec ( G , (/) ) ` suc b ) " c ) ) ) |
59 |
|
fvex |
|- ( rec ( G , (/) ) ` suc b ) e. _V |
60 |
59
|
resex |
|- ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) e. _V |
61 |
|
dmeq |
|- ( x = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> dom x = dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) |
62 |
61
|
pweqd |
|- ( x = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ~P dom x = ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) |
63 |
|
imaeq1 |
|- ( x = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ( x " y ) = ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) |
64 |
63
|
fveq2d |
|- ( x = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ( F ` ( x " y ) ) = ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) |
65 |
62 64
|
mpteq12dv |
|- ( x = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) = ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) ) |
66 |
60
|
dmex |
|- dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) e. _V |
67 |
66
|
pwex |
|- ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) e. _V |
68 |
67
|
mptex |
|- ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) e. _V |
69 |
65 2 68
|
fvmpt |
|- ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) e. _V -> ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) = ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) ) |
70 |
60 69
|
ax-mp |
|- ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) = ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) |
71 |
70
|
fveq1i |
|- ( ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ` c ) = ( ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) ` c ) |
72 |
|
r1sssuc |
|- ( b e. On -> ( R1 ` b ) C_ ( R1 ` suc b ) ) |
73 |
50 72
|
syl |
|- ( b e. _om -> ( R1 ` b ) C_ ( R1 ` suc b ) ) |
74 |
|
fnssres |
|- ( ( ( rec ( G , (/) ) ` suc b ) Fn ( R1 ` suc b ) /\ ( R1 ` b ) C_ ( R1 ` suc b ) ) -> ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) Fn ( R1 ` b ) ) |
75 |
37 73 74
|
syl2anc |
|- ( b e. _om -> ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) Fn ( R1 ` b ) ) |
76 |
75
|
fndmd |
|- ( b e. _om -> dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) = ( R1 ` b ) ) |
77 |
76
|
pweqd |
|- ( b e. _om -> ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) = ~P ( R1 ` b ) ) |
78 |
77
|
adantr |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) = ~P ( R1 ` b ) ) |
79 |
54 78
|
eleqtrrd |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> c e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) |
80 |
|
imaeq2 |
|- ( y = c -> ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) = ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) ) |
81 |
80
|
fveq2d |
|- ( y = c -> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) = ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) ) ) |
82 |
|
eqid |
|- ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) = ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) |
83 |
|
fvex |
|- ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) ) e. _V |
84 |
81 82 83
|
fvmpt |
|- ( c e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ( ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) ` c ) = ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) ) ) |
85 |
79 84
|
syl |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ( ( y e. ~P dom ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) |-> ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " y ) ) ) ` c ) = ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) ) ) |
86 |
71 85
|
eqtrid |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ( ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ` c ) = ( F ` ( ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) " c ) ) ) |
87 |
|
dmeq |
|- ( x = ( rec ( G , (/) ) ` suc b ) -> dom x = dom ( rec ( G , (/) ) ` suc b ) ) |
88 |
87
|
pweqd |
|- ( x = ( rec ( G , (/) ) ` suc b ) -> ~P dom x = ~P dom ( rec ( G , (/) ) ` suc b ) ) |
89 |
|
imaeq1 |
|- ( x = ( rec ( G , (/) ) ` suc b ) -> ( x " y ) = ( ( rec ( G , (/) ) ` suc b ) " y ) ) |
90 |
89
|
fveq2d |
|- ( x = ( rec ( G , (/) ) ` suc b ) -> ( F ` ( x " y ) ) = ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) |
91 |
88 90
|
mpteq12dv |
|- ( x = ( rec ( G , (/) ) ` suc b ) -> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) ) |
92 |
59
|
dmex |
|- dom ( rec ( G , (/) ) ` suc b ) e. _V |
93 |
92
|
pwex |
|- ~P dom ( rec ( G , (/) ) ` suc b ) e. _V |
94 |
93
|
mptex |
|- ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) e. _V |
95 |
91 2 94
|
fvmpt |
|- ( ( rec ( G , (/) ) ` suc b ) e. _V -> ( G ` ( rec ( G , (/) ) ` suc b ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) ) |
96 |
59 95
|
ax-mp |
|- ( G ` ( rec ( G , (/) ) ` suc b ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) |
97 |
96
|
fveq1i |
|- ( ( G ` ( rec ( G , (/) ) ` suc b ) ) ` c ) = ( ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) ` c ) |
98 |
|
r1tr |
|- Tr ( R1 ` suc b ) |
99 |
98
|
a1i |
|- ( b e. _om -> Tr ( R1 ` suc b ) ) |
100 |
|
dftr4 |
|- ( Tr ( R1 ` suc b ) <-> ( R1 ` suc b ) C_ ~P ( R1 ` suc b ) ) |
101 |
99 100
|
sylib |
|- ( b e. _om -> ( R1 ` suc b ) C_ ~P ( R1 ` suc b ) ) |
102 |
101
|
sselda |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> c e. ~P ( R1 ` suc b ) ) |
103 |
|
f1odm |
|- ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) -> dom ( rec ( G , (/) ) ` suc b ) = ( R1 ` suc b ) ) |
104 |
35 103
|
syl |
|- ( b e. _om -> dom ( rec ( G , (/) ) ` suc b ) = ( R1 ` suc b ) ) |
105 |
104
|
pweqd |
|- ( b e. _om -> ~P dom ( rec ( G , (/) ) ` suc b ) = ~P ( R1 ` suc b ) ) |
106 |
105
|
adantr |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ~P dom ( rec ( G , (/) ) ` suc b ) = ~P ( R1 ` suc b ) ) |
107 |
102 106
|
eleqtrrd |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> c e. ~P dom ( rec ( G , (/) ) ` suc b ) ) |
108 |
|
imaeq2 |
|- ( y = c -> ( ( rec ( G , (/) ) ` suc b ) " y ) = ( ( rec ( G , (/) ) ` suc b ) " c ) ) |
109 |
108
|
fveq2d |
|- ( y = c -> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) = ( F ` ( ( rec ( G , (/) ) ` suc b ) " c ) ) ) |
110 |
|
eqid |
|- ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) |
111 |
|
fvex |
|- ( F ` ( ( rec ( G , (/) ) ` suc b ) " c ) ) e. _V |
112 |
109 110 111
|
fvmpt |
|- ( c e. ~P dom ( rec ( G , (/) ) ` suc b ) -> ( ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) ` c ) = ( F ` ( ( rec ( G , (/) ) ` suc b ) " c ) ) ) |
113 |
107 112
|
syl |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ( ( y e. ~P dom ( rec ( G , (/) ) ` suc b ) |-> ( F ` ( ( rec ( G , (/) ) ` suc b ) " y ) ) ) ` c ) = ( F ` ( ( rec ( G , (/) ) ` suc b ) " c ) ) ) |
114 |
97 113
|
eqtrid |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ( ( G ` ( rec ( G , (/) ) ` suc b ) ) ` c ) = ( F ` ( ( rec ( G , (/) ) ` suc b ) " c ) ) ) |
115 |
58 86 114
|
3eqtr4d |
|- ( ( b e. _om /\ c e. ( R1 ` suc b ) ) -> ( ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ` c ) = ( ( G ` ( rec ( G , (/) ) ` suc b ) ) ` c ) ) |
116 |
115
|
adantlr |
|- ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) /\ c e. ( R1 ` suc b ) ) -> ( ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ` c ) = ( ( G ` ( rec ( G , (/) ) ` suc b ) ) ` c ) ) |
117 |
|
fveq2 |
|- ( ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ( G ` ( rec ( G , (/) ) ` b ) ) = ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ) |
118 |
117
|
fveq1d |
|- ( ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ( ( G ` ( rec ( G , (/) ) ` b ) ) ` c ) = ( ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ` c ) ) |
119 |
118
|
ad2antlr |
|- ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) /\ c e. ( R1 ` suc b ) ) -> ( ( G ` ( rec ( G , (/) ) ` b ) ) ` c ) = ( ( G ` ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) ` c ) ) |
120 |
|
rdgsuc |
|- ( suc b e. On -> ( rec ( G , (/) ) ` suc suc b ) = ( G ` ( rec ( G , (/) ) ` suc b ) ) ) |
121 |
44 120
|
syl |
|- ( b e. _om -> ( rec ( G , (/) ) ` suc suc b ) = ( G ` ( rec ( G , (/) ) ` suc b ) ) ) |
122 |
121
|
fveq1d |
|- ( b e. _om -> ( ( rec ( G , (/) ) ` suc suc b ) ` c ) = ( ( G ` ( rec ( G , (/) ) ` suc b ) ) ` c ) ) |
123 |
122
|
ad2antrr |
|- ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) /\ c e. ( R1 ` suc b ) ) -> ( ( rec ( G , (/) ) ` suc suc b ) ` c ) = ( ( G ` ( rec ( G , (/) ) ` suc b ) ) ` c ) ) |
124 |
116 119 123
|
3eqtr4rd |
|- ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) /\ c e. ( R1 ` suc b ) ) -> ( ( rec ( G , (/) ) ` suc suc b ) ` c ) = ( ( G ` ( rec ( G , (/) ) ` b ) ) ` c ) ) |
125 |
|
fvres |
|- ( c e. ( R1 ` suc b ) -> ( ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) ` c ) = ( ( rec ( G , (/) ) ` suc suc b ) ` c ) ) |
126 |
125
|
adantl |
|- ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) /\ c e. ( R1 ` suc b ) ) -> ( ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) ` c ) = ( ( rec ( G , (/) ) ` suc suc b ) ` c ) ) |
127 |
|
rdgsuc |
|- ( b e. On -> ( rec ( G , (/) ) ` suc b ) = ( G ` ( rec ( G , (/) ) ` b ) ) ) |
128 |
50 127
|
syl |
|- ( b e. _om -> ( rec ( G , (/) ) ` suc b ) = ( G ` ( rec ( G , (/) ) ` b ) ) ) |
129 |
128
|
fveq1d |
|- ( b e. _om -> ( ( rec ( G , (/) ) ` suc b ) ` c ) = ( ( G ` ( rec ( G , (/) ) ` b ) ) ` c ) ) |
130 |
129
|
ad2antrr |
|- ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) /\ c e. ( R1 ` suc b ) ) -> ( ( rec ( G , (/) ) ` suc b ) ` c ) = ( ( G ` ( rec ( G , (/) ) ` b ) ) ` c ) ) |
131 |
124 126 130
|
3eqtr4rd |
|- ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) /\ c e. ( R1 ` suc b ) ) -> ( ( rec ( G , (/) ) ` suc b ) ` c ) = ( ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) ` c ) ) |
132 |
38 49 131
|
eqfnfvd |
|- ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) ) -> ( rec ( G , (/) ) ` suc b ) = ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) ) |
133 |
132
|
ex |
|- ( b e. _om -> ( ( rec ( G , (/) ) ` b ) = ( ( rec ( G , (/) ) ` suc b ) |` ( R1 ` b ) ) -> ( rec ( G , (/) ) ` suc b ) = ( ( rec ( G , (/) ) ` suc suc b ) |` ( R1 ` suc b ) ) ) ) |
134 |
8 14 20 26 32 133
|
finds |
|- ( A e. _om -> ( rec ( G , (/) ) ` A ) = ( ( rec ( G , (/) ) ` suc A ) |` ( R1 ` A ) ) ) |
135 |
|
resss |
|- ( ( rec ( G , (/) ) ` suc A ) |` ( R1 ` A ) ) C_ ( rec ( G , (/) ) ` suc A ) |
136 |
134 135
|
eqsstrdi |
|- ( A e. _om -> ( rec ( G , (/) ) ` A ) C_ ( rec ( G , (/) ) ` suc A ) ) |