Metamath Proof Explorer

Theorem ackbij2lem3

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypotheses ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
ackbij.g 
|- G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) )
Assertion ackbij2lem3 
|- ( A e. _om -> ( rec ( G , (/) ) ` A ) C_ ( rec ( G , (/) ) ` suc A ) )

Proof

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 ) )