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