Metamath Proof Explorer

Theorem fseqenlem1

Description: Lemma for fseqen . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Hypotheses fseqenlem.a 
|- ( ph -> A e. V )
fseqenlem.b 
|- ( ph -> B e. A )
fseqenlem.f 
|- ( ph -> F : ( A X. A ) -1-1-onto-> A )
fseqenlem.g 
|- G = seqom ( ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) , { <. (/) , B >. } )
Assertion fseqenlem1 
|- ( ( ph /\ C e. _om ) -> ( G ` C ) : ( A ^m C ) -1-1-> A )

Proof

Step Hyp Ref Expression
1 fseqenlem.a 
 |-  ( ph -> A e. V )
2 fseqenlem.b 
 |-  ( ph -> B e. A )
3 fseqenlem.f 
 |-  ( ph -> F : ( A X. A ) -1-1-onto-> A )
4 fseqenlem.g 
 |-  G = seqom ( ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) , { <. (/) , B >. } )
5 fveq2 
 |-  ( y = C -> ( G ` y ) = ( G ` C ) )
6 f1eq1 
 |-  ( ( G ` y ) = ( G ` C ) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m y ) -1-1-> A ) )
7 5 6 syl 
 |-  ( y = C -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m y ) -1-1-> A ) )
8 oveq2 
 |-  ( y = C -> ( A ^m y ) = ( A ^m C ) )
9 f1eq2 
 |-  ( ( A ^m y ) = ( A ^m C ) -> ( ( G ` C ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
10 8 9 syl 
 |-  ( y = C -> ( ( G ` C ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
11 7 10 bitrd 
 |-  ( y = C -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
12 11 imbi2d 
 |-  ( y = C -> ( ( ph -> ( G ` y ) : ( A ^m y ) -1-1-> A ) <-> ( ph -> ( G ` C ) : ( A ^m C ) -1-1-> A ) ) )
13 fveq2 
 |-  ( y = (/) -> ( G ` y ) = ( G ` (/) ) )
14 snex 
 |-  { <. (/) , B >. } e. _V
15 4 seqom0g 
 |-  ( { <. (/) , B >. } e. _V -> ( G ` (/) ) = { <. (/) , B >. } )
16 14 15 ax-mp 
 |-  ( G ` (/) ) = { <. (/) , B >. }
17 13 16 eqtrdi 
 |-  ( y = (/) -> ( G ` y ) = { <. (/) , B >. } )
18 f1eq1 
 |-  ( ( G ` y ) = { <. (/) , B >. } -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m y ) -1-1-> A ) )
19 17 18 syl 
 |-  ( y = (/) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m y ) -1-1-> A ) )
20 oveq2 
 |-  ( y = (/) -> ( A ^m y ) = ( A ^m (/) ) )
21 f1eq2 
 |-  ( ( A ^m y ) = ( A ^m (/) ) -> ( { <. (/) , B >. } : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A ) )
22 20 21 syl 
 |-  ( y = (/) -> ( { <. (/) , B >. } : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A ) )
23 19 22 bitrd 
 |-  ( y = (/) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A ) )
24 fveq2 
 |-  ( y = m -> ( G ` y ) = ( G ` m ) )
25 f1eq1 
 |-  ( ( G ` y ) = ( G ` m ) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m y ) -1-1-> A ) )
26 24 25 syl 
 |-  ( y = m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m y ) -1-1-> A ) )
27 oveq2 
 |-  ( y = m -> ( A ^m y ) = ( A ^m m ) )
28 f1eq2 
 |-  ( ( A ^m y ) = ( A ^m m ) -> ( ( G ` m ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m m ) -1-1-> A ) )
29 27 28 syl 
 |-  ( y = m -> ( ( G ` m ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m m ) -1-1-> A ) )
30 26 29 bitrd 
 |-  ( y = m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m m ) -1-1-> A ) )
31 fveq2 
 |-  ( y = suc m -> ( G ` y ) = ( G ` suc m ) )
32 f1eq1 
 |-  ( ( G ` y ) = ( G ` suc m ) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m y ) -1-1-> A ) )
33 31 32 syl 
 |-  ( y = suc m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m y ) -1-1-> A ) )
34 oveq2 
 |-  ( y = suc m -> ( A ^m y ) = ( A ^m suc m ) )
35 f1eq2 
 |-  ( ( A ^m y ) = ( A ^m suc m ) -> ( ( G ` suc m ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) )
36 34 35 syl 
 |-  ( y = suc m -> ( ( G ` suc m ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) )
37 33 36 bitrd 
 |-  ( y = suc m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) )
38 0ex 
 |-  (/) e. _V
39 f1osng 
 |-  ( ( (/) e. _V /\ B e. A ) -> { <. (/) , B >. } : { (/) } -1-1-onto-> { B } )
40 38 2 39 sylancr 
 |-  ( ph -> { <. (/) , B >. } : { (/) } -1-1-onto-> { B } )
41 f1of1 
 |-  ( { <. (/) , B >. } : { (/) } -1-1-onto-> { B } -> { <. (/) , B >. } : { (/) } -1-1-> { B } )
42 40 41 syl 
 |-  ( ph -> { <. (/) , B >. } : { (/) } -1-1-> { B } )
43 2 snssd 
 |-  ( ph -> { B } C_ A )
44 f1ss 
 |-  ( ( { <. (/) , B >. } : { (/) } -1-1-> { B } /\ { B } C_ A ) -> { <. (/) , B >. } : { (/) } -1-1-> A )
45 42 43 44 syl2anc 
 |-  ( ph -> { <. (/) , B >. } : { (/) } -1-1-> A )
46 map0e 
 |-  ( A e. V -> ( A ^m (/) ) = 1o )
47 1 46 syl 
 |-  ( ph -> ( A ^m (/) ) = 1o )
48 df1o2 
 |-  1o = { (/) }
49 47 48 eqtrdi 
 |-  ( ph -> ( A ^m (/) ) = { (/) } )
50 f1eq2 
 |-  ( ( A ^m (/) ) = { (/) } -> ( { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A <-> { <. (/) , B >. } : { (/) } -1-1-> A ) )
51 49 50 syl 
 |-  ( ph -> ( { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A <-> { <. (/) , B >. } : { (/) } -1-1-> A ) )
52 45 51 mpbird 
 |-  ( ph -> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A )
53 4 seqomsuc 
 |-  ( m e. _om -> ( G ` suc m ) = ( m ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) ( G ` m ) ) )
54 53 ad2antrl 
 |-  ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` suc m ) = ( m ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) ( G ` m ) ) )
55 vex 
 |-  m e. _V
56 fvex 
 |-  ( G ` m ) e. _V
57 reseq1 
 |-  ( x = z -> ( x |` a ) = ( z |` a ) )
58 57 fveq2d 
 |-  ( x = z -> ( b ` ( x |` a ) ) = ( b ` ( z |` a ) ) )
59 fveq1 
 |-  ( x = z -> ( x ` a ) = ( z ` a ) )
60 58 59 oveq12d 
 |-  ( x = z -> ( ( b ` ( x |` a ) ) F ( x ` a ) ) = ( ( b ` ( z |` a ) ) F ( z ` a ) ) )
61 60 cbvmptv 
 |-  ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) ) = ( z e. ( A ^m suc a ) |-> ( ( b ` ( z |` a ) ) F ( z ` a ) ) )
62 suceq 
 |-  ( a = m -> suc a = suc m )
63 62 adantr 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> suc a = suc m )
64 63 oveq2d 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> ( A ^m suc a ) = ( A ^m suc m ) )
65 simpr 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> b = ( G ` m ) )
66 reseq2 
 |-  ( a = m -> ( z |` a ) = ( z |` m ) )
67 66 adantr 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> ( z |` a ) = ( z |` m ) )
68 65 67 fveq12d 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> ( b ` ( z |` a ) ) = ( ( G ` m ) ` ( z |` m ) ) )
69 simpl 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> a = m )
70 69 fveq2d 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> ( z ` a ) = ( z ` m ) )
71 68 70 oveq12d 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> ( ( b ` ( z |` a ) ) F ( z ` a ) ) = ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) )
72 64 71 mpteq12dv 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> ( z e. ( A ^m suc a ) |-> ( ( b ` ( z |` a ) ) F ( z ` a ) ) ) = ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) )
73 61 72 eqtrid 
 |-  ( ( a = m /\ b = ( G ` m ) ) -> ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) ) = ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) )
74 nfcv 
 |-  F/_ a ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) )
75 nfcv 
 |-  F/_ b ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) )
76 nfcv 
 |-  F/_ n ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) )
77 nfcv 
 |-  F/_ f ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) )
78 suceq 
 |-  ( n = a -> suc n = suc a )
79 78 adantr 
 |-  ( ( n = a /\ f = b ) -> suc n = suc a )
80 79 oveq2d 
 |-  ( ( n = a /\ f = b ) -> ( A ^m suc n ) = ( A ^m suc a ) )
81 simpr 
 |-  ( ( n = a /\ f = b ) -> f = b )
82 reseq2 
 |-  ( n = a -> ( x |` n ) = ( x |` a ) )
83 82 adantr 
 |-  ( ( n = a /\ f = b ) -> ( x |` n ) = ( x |` a ) )
84 81 83 fveq12d 
 |-  ( ( n = a /\ f = b ) -> ( f ` ( x |` n ) ) = ( b ` ( x |` a ) ) )
85 simpl 
 |-  ( ( n = a /\ f = b ) -> n = a )
86 85 fveq2d 
 |-  ( ( n = a /\ f = b ) -> ( x ` n ) = ( x ` a ) )
87 84 86 oveq12d 
 |-  ( ( n = a /\ f = b ) -> ( ( f ` ( x |` n ) ) F ( x ` n ) ) = ( ( b ` ( x |` a ) ) F ( x ` a ) ) )
88 80 87 mpteq12dv 
 |-  ( ( n = a /\ f = b ) -> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) = ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) ) )
89 74 75 76 77 88 cbvmpo 
 |-  ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) = ( a e. _V , b e. _V |-> ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) ) )
90 ovex 
 |-  ( A ^m suc m ) e. _V
91 90 mptex 
 |-  ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) e. _V
92 73 89 91 ovmpoa 
 |-  ( ( m e. _V /\ ( G ` m ) e. _V ) -> ( m ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) ( G ` m ) ) = ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) )
93 55 56 92 mp2an 
 |-  ( m ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) ( G ` m ) ) = ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) )
94 54 93 eqtrdi 
 |-  ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` suc m ) = ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) )
95 3 ad2antrr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> F : ( A X. A ) -1-1-onto-> A )
96 f1of 
 |-  ( F : ( A X. A ) -1-1-onto-> A -> F : ( A X. A ) --> A )
97 95 96 syl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> F : ( A X. A ) --> A )
98 f1f 
 |-  ( ( G ` m ) : ( A ^m m ) -1-1-> A -> ( G ` m ) : ( A ^m m ) --> A )
99 98 ad2antll 
 |-  ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` m ) : ( A ^m m ) --> A )
100 99 adantr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( G ` m ) : ( A ^m m ) --> A )
101 elmapi 
 |-  ( z e. ( A ^m suc m ) -> z : suc m --> A )
102 101 adantl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> z : suc m --> A )
103 sssucid 
 |-  m C_ suc m
104 fssres 
 |-  ( ( z : suc m --> A /\ m C_ suc m ) -> ( z |` m ) : m --> A )
105 102 103 104 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( z |` m ) : m --> A )
106 1 ad2antrr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> A e. V )
107 elmapg 
 |-  ( ( A e. V /\ m e. _V ) -> ( ( z |` m ) e. ( A ^m m ) <-> ( z |` m ) : m --> A ) )
108 106 55 107 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( ( z |` m ) e. ( A ^m m ) <-> ( z |` m ) : m --> A ) )
109 105 108 mpbird 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( z |` m ) e. ( A ^m m ) )
110 100 109 ffvelrnd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( ( G ` m ) ` ( z |` m ) ) e. A )
111 55 sucid 
 |-  m e. suc m
112 ffvelrn 
 |-  ( ( z : suc m --> A /\ m e. suc m ) -> ( z ` m ) e. A )
113 102 111 112 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( z ` m ) e. A )
114 97 110 113 fovrnd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) e. A )
115 94 114 fmpt3d 
 |-  ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` suc m ) : ( A ^m suc m ) --> A )
116 elmapi 
 |-  ( a e. ( A ^m suc m ) -> a : suc m --> A )
117 116 ad2antrl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> a : suc m --> A )
118 117 ffnd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> a Fn suc m )
119 elmapi 
 |-  ( b e. ( A ^m suc m ) -> b : suc m --> A )
120 119 ad2antll 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> b : suc m --> A )
121 120 ffnd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> b Fn suc m )
122 103 a1i 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> m C_ suc m )
123 fvreseq 
 |-  ( ( ( a Fn suc m /\ b Fn suc m ) /\ m C_ suc m ) -> ( ( a |` m ) = ( b |` m ) <-> A. x e. m ( a ` x ) = ( b ` x ) ) )
124 118 121 122 123 syl21anc 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( a |` m ) = ( b |` m ) <-> A. x e. m ( a ` x ) = ( b ` x ) ) )
125 fveq2 
 |-  ( x = m -> ( a ` x ) = ( a ` m ) )
126 fveq2 
 |-  ( x = m -> ( b ` x ) = ( b ` m ) )
127 125 126 eqeq12d 
 |-  ( x = m -> ( ( a ` x ) = ( b ` x ) <-> ( a ` m ) = ( b ` m ) ) )
128 55 127 ralsn 
 |-  ( A. x e. { m } ( a ` x ) = ( b ` x ) <-> ( a ` m ) = ( b ` m ) )
129 128 bicomi 
 |-  ( ( a ` m ) = ( b ` m ) <-> A. x e. { m } ( a ` x ) = ( b ` x ) )
130 129 a1i 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( a ` m ) = ( b ` m ) <-> A. x e. { m } ( a ` x ) = ( b ` x ) ) )
131 124 130 anbi12d 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( ( a |` m ) = ( b |` m ) /\ ( a ` m ) = ( b ` m ) ) <-> ( A. x e. m ( a ` x ) = ( b ` x ) /\ A. x e. { m } ( a ` x ) = ( b ` x ) ) ) )
132 94 adantr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( G ` suc m ) = ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) )
133 132 fveq1d 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` suc m ) ` a ) = ( ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) ` a ) )
134 reseq1 
 |-  ( z = a -> ( z |` m ) = ( a |` m ) )
135 134 fveq2d 
 |-  ( z = a -> ( ( G ` m ) ` ( z |` m ) ) = ( ( G ` m ) ` ( a |` m ) ) )
136 fveq1 
 |-  ( z = a -> ( z ` m ) = ( a ` m ) )
137 135 136 oveq12d 
 |-  ( z = a -> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) = ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) )
138 eqid 
 |-  ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) = ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) )
139 ovex 
 |-  ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) e. _V
140 137 138 139 fvmpt 
 |-  ( a e. ( A ^m suc m ) -> ( ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) ` a ) = ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) )
141 140 ad2antrl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) ` a ) = ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) )
142 133 141 eqtrd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` suc m ) ` a ) = ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) )
143 df-ov 
 |-  ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) = ( F ` <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. )
144 142 143 eqtrdi 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` suc m ) ` a ) = ( F ` <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. ) )
145 132 fveq1d 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` suc m ) ` b ) = ( ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) ` b ) )
146 reseq1 
 |-  ( z = b -> ( z |` m ) = ( b |` m ) )
147 146 fveq2d 
 |-  ( z = b -> ( ( G ` m ) ` ( z |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) )
148 fveq1 
 |-  ( z = b -> ( z ` m ) = ( b ` m ) )
149 147 148 oveq12d 
 |-  ( z = b -> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) = ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) )
150 ovex 
 |-  ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) e. _V
151 149 138 150 fvmpt 
 |-  ( b e. ( A ^m suc m ) -> ( ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) ` b ) = ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) )
152 151 ad2antll 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) ` b ) = ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) )
153 145 152 eqtrd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` suc m ) ` b ) = ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) )
154 df-ov 
 |-  ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) = ( F ` <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. )
155 153 154 eqtrdi 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` suc m ) ` b ) = ( F ` <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. ) )
156 144 155 eqeq12d 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( ( G ` suc m ) ` a ) = ( ( G ` suc m ) ` b ) <-> ( F ` <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. ) = ( F ` <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. ) ) )
157 3 ad2antrr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> F : ( A X. A ) -1-1-onto-> A )
158 f1of1 
 |-  ( F : ( A X. A ) -1-1-onto-> A -> F : ( A X. A ) -1-1-> A )
159 157 158 syl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> F : ( A X. A ) -1-1-> A )
160 99 adantr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( G ` m ) : ( A ^m m ) --> A )
161 fssres 
 |-  ( ( a : suc m --> A /\ m C_ suc m ) -> ( a |` m ) : m --> A )
162 117 103 161 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( a |` m ) : m --> A )
163 1 ad2antrr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> A e. V )
164 elmapg 
 |-  ( ( A e. V /\ m e. _V ) -> ( ( a |` m ) e. ( A ^m m ) <-> ( a |` m ) : m --> A ) )
165 163 55 164 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( a |` m ) e. ( A ^m m ) <-> ( a |` m ) : m --> A ) )
166 162 165 mpbird 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( a |` m ) e. ( A ^m m ) )
167 160 166 ffvelrnd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` m ) ` ( a |` m ) ) e. A )
168 ffvelrn 
 |-  ( ( a : suc m --> A /\ m e. suc m ) -> ( a ` m ) e. A )
169 117 111 168 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( a ` m ) e. A )
170 167 169 opelxpd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. e. ( A X. A ) )
171 fssres 
 |-  ( ( b : suc m --> A /\ m C_ suc m ) -> ( b |` m ) : m --> A )
172 120 103 171 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( b |` m ) : m --> A )
173 elmapg 
 |-  ( ( A e. V /\ m e. _V ) -> ( ( b |` m ) e. ( A ^m m ) <-> ( b |` m ) : m --> A ) )
174 163 55 173 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( b |` m ) e. ( A ^m m ) <-> ( b |` m ) : m --> A ) )
175 172 174 mpbird 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( b |` m ) e. ( A ^m m ) )
176 160 175 ffvelrnd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( G ` m ) ` ( b |` m ) ) e. A )
177 ffvelrn 
 |-  ( ( b : suc m --> A /\ m e. suc m ) -> ( b ` m ) e. A )
178 120 111 177 sylancl 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( b ` m ) e. A )
179 176 178 opelxpd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. e. ( A X. A ) )
180 f1fveq 
 |-  ( ( F : ( A X. A ) -1-1-> A /\ ( <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. e. ( A X. A ) /\ <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. e. ( A X. A ) ) ) -> ( ( F ` <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. ) = ( F ` <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. ) <-> <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. = <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. ) )
181 159 170 179 180 syl12anc 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( F ` <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. ) = ( F ` <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. ) <-> <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. = <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. ) )
182 fvex 
 |-  ( ( G ` m ) ` ( a |` m ) ) e. _V
183 fvex 
 |-  ( a ` m ) e. _V
184 182 183 opth 
 |-  ( <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. = <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. <-> ( ( ( G ` m ) ` ( a |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) /\ ( a ` m ) = ( b ` m ) ) )
185 181 184 bitrdi 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( F ` <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. ) = ( F ` <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. ) <-> ( ( ( G ` m ) ` ( a |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) /\ ( a ` m ) = ( b ` m ) ) ) )
186 simplrr 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( G ` m ) : ( A ^m m ) -1-1-> A )
187 f1fveq 
 |-  ( ( ( G ` m ) : ( A ^m m ) -1-1-> A /\ ( ( a |` m ) e. ( A ^m m ) /\ ( b |` m ) e. ( A ^m m ) ) ) -> ( ( ( G ` m ) ` ( a |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) <-> ( a |` m ) = ( b |` m ) ) )
188 186 166 175 187 syl12anc 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( ( G ` m ) ` ( a |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) <-> ( a |` m ) = ( b |` m ) ) )
189 188 anbi1d 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( ( ( G ` m ) ` ( a |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) /\ ( a ` m ) = ( b ` m ) ) <-> ( ( a |` m ) = ( b |` m ) /\ ( a ` m ) = ( b ` m ) ) ) )
190 156 185 189 3bitrd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( ( G ` suc m ) ` a ) = ( ( G ` suc m ) ` b ) <-> ( ( a |` m ) = ( b |` m ) /\ ( a ` m ) = ( b ` m ) ) ) )
191 eqfnfv 
 |-  ( ( a Fn suc m /\ b Fn suc m ) -> ( a = b <-> A. x e. suc m ( a ` x ) = ( b ` x ) ) )
192 118 121 191 syl2anc 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( a = b <-> A. x e. suc m ( a ` x ) = ( b ` x ) ) )
193 df-suc 
 |-  suc m = ( m u. { m } )
194 193 raleqi 
 |-  ( A. x e. suc m ( a ` x ) = ( b ` x ) <-> A. x e. ( m u. { m } ) ( a ` x ) = ( b ` x ) )
195 ralunb 
 |-  ( A. x e. ( m u. { m } ) ( a ` x ) = ( b ` x ) <-> ( A. x e. m ( a ` x ) = ( b ` x ) /\ A. x e. { m } ( a ` x ) = ( b ` x ) ) )
196 194 195 bitri 
 |-  ( A. x e. suc m ( a ` x ) = ( b ` x ) <-> ( A. x e. m ( a ` x ) = ( b ` x ) /\ A. x e. { m } ( a ` x ) = ( b ` x ) ) )
197 192 196 bitrdi 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( a = b <-> ( A. x e. m ( a ` x ) = ( b ` x ) /\ A. x e. { m } ( a ` x ) = ( b ` x ) ) ) )
198 131 190 197 3bitr4d 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( ( G ` suc m ) ` a ) = ( ( G ` suc m ) ` b ) <-> a = b ) )
199 198 biimpd 
 |-  ( ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ ( a e. ( A ^m suc m ) /\ b e. ( A ^m suc m ) ) ) -> ( ( ( G ` suc m ) ` a ) = ( ( G ` suc m ) ` b ) -> a = b ) )
200 199 ralrimivva 
 |-  ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> A. a e. ( A ^m suc m ) A. b e. ( A ^m suc m ) ( ( ( G ` suc m ) ` a ) = ( ( G ` suc m ) ` b ) -> a = b ) )
201 dff13 
 |-  ( ( G ` suc m ) : ( A ^m suc m ) -1-1-> A <-> ( ( G ` suc m ) : ( A ^m suc m ) --> A /\ A. a e. ( A ^m suc m ) A. b e. ( A ^m suc m ) ( ( ( G ` suc m ) ` a ) = ( ( G ` suc m ) ` b ) -> a = b ) ) )
202 115 200 201 sylanbrc 
 |-  ( ( ph /\ ( m e. _om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A )
203 202 expr 
 |-  ( ( ph /\ m e. _om ) -> ( ( G ` m ) : ( A ^m m ) -1-1-> A -> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) )
204 203 expcom 
 |-  ( m e. _om -> ( ph -> ( ( G ` m ) : ( A ^m m ) -1-1-> A -> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) ) )
205 23 30 37 52 204 finds2 
 |-  ( y e. _om -> ( ph -> ( G ` y ) : ( A ^m y ) -1-1-> A ) )
206 12 205 vtoclga 
 |-  ( C e. _om -> ( ph -> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
207 206 impcom 
 |-  ( ( ph /\ C e. _om ) -> ( G ` C ) : ( A ^m C ) -1-1-> A )