MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fseqenlem1 Structured version   Visualization version   Unicode version
Theorem fseqenlem1 8847
Description: Lemma for fseqen 8850. (Contributed by Mario Carneiro, 17-May-2015.)
Hypotheses
Ref Expression
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 = seq𝜔 ( ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) , { <. (/) , B >. } )
Assertion
Ref Expression
fseqenlem1 |- ( ( ph /\ C e. om ) -> ( G ` C ) : ( A ^m C ) -1-1-> A )
Distinct variable groups:   f, n, x, F   A, f, n, x   ph, n, x
Allowed substitution hints:   ph( f)   B( x, f, n)   C( x, f, n)   G( x, f, n)   V( x, f, n)
Proof of Theorem fseqenlem1
Dummy variables y a b z m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6191 . . . . . 6 |- ( y = C -> ( G ` y ) = ( G ` C ) )
2 f1eq1 6096 . . . . . 6 |- ( ( G ` y ) = ( G ` C ) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m y ) -1-1-> A ) )
31, 2syl 17 . . . . 5 |- ( y = C -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m y ) -1-1-> A ) )
4 oveq2 6658 . . . . . 6 |- ( y = C -> ( A ^m y ) = ( A ^m C ) )
5 f1eq2 6097 . . . . . 6 |- ( ( A ^m y ) = ( A ^m C ) -> ( ( G ` C ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
64, 5syl 17 . . . . 5 |- ( y = C -> ( ( G ` C ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
73, 6bitrd 268 . . . 4 |- ( y = C -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
87imbi2d 330 . . 3 |- ( y = C -> ( ( ph -> ( G ` y ) : ( A ^m y ) -1-1-> A ) <-> ( ph -> ( G ` C ) : ( A ^m C ) -1-1-> A ) ) )
9 fveq2 6191 . . . . . . 7 |- ( y = (/) -> ( G ` y ) = ( G ` (/) ) )
10 snex 4908 . . . . . . . 8 |- { <. (/) , B >. } e. _V
11 fseqenlem.g . . . . . . . . 9 |- G = seq𝜔 ( ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) , { <. (/) , B >. } )
1211seqom0g 7551 . . . . . . . 8 |- ( { <. (/) , B >. } e. _V -> ( G ` (/) ) = { <. (/) , B >. } )
1310, 12ax-mp 5 . . . . . . 7 |- ( G ` (/) ) = { <. (/) , B >. }
149, 13syl6eq 2672 . . . . . 6 |- ( y = (/) -> ( G ` y ) = { <. (/) , B >. } )
15 f1eq1 6096 . . . . . 6 |- ( ( G ` y ) = { <. (/) , B >. } -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m y ) -1-1-> A ) )
1614, 15syl 17 . . . . 5 |- ( y = (/) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m y ) -1-1-> A ) )
17 oveq2 6658 . . . . . 6 |- ( y = (/) -> ( A ^m y ) = ( A ^m (/) ) )
18 f1eq2 6097 . . . . . 6 |- ( ( A ^m y ) = ( A ^m (/) ) -> ( { <. (/) , B >. } : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A ) )
1917, 18syl 17 . . . . 5 |- ( y = (/) -> ( { <. (/) , B >. } : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A ) )
2016, 19bitrd 268 . . . 4 |- ( y = (/) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A ) )
21 fveq2 6191 . . . . . 6 |- ( y = m -> ( G ` y ) = ( G ` m ) )
22 f1eq1 6096 . . . . . 6 |- ( ( G ` y ) = ( G ` m ) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m y ) -1-1-> A ) )
2321, 22syl 17 . . . . 5 |- ( y = m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m y ) -1-1-> A ) )
24 oveq2 6658 . . . . . 6 |- ( y = m -> ( A ^m y ) = ( A ^m m ) )
25 f1eq2 6097 . . . . . 6 |- ( ( A ^m y ) = ( A ^m m ) -> ( ( G ` m ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m m ) -1-1-> A ) )
2624, 25syl 17 . . . . 5 |- ( y = m -> ( ( G ` m ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m m ) -1-1-> A ) )
2723, 26bitrd 268 . . . 4 |- ( y = m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` m ) : ( A ^m m ) -1-1-> A ) )
28 fveq2 6191 . . . . . 6 |- ( y = suc m -> ( G ` y ) = ( G ` suc m ) )
29 f1eq1 6096 . . . . . 6 |- ( ( G ` y ) = ( G ` suc m ) -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m y ) -1-1-> A ) )
3028, 29syl 17 . . . . 5 |- ( y = suc m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m y ) -1-1-> A ) )
31 oveq2 6658 . . . . . 6 |- ( y = suc m -> ( A ^m y ) = ( A ^m suc m ) )
32 f1eq2 6097 . . . . . 6 |- ( ( 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 ) )
3331, 32syl 17 . . . . 5 |- ( y = suc m -> ( ( G ` suc m ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) )
3430, 33bitrd 268 . . . 4 |- ( y = suc m -> ( ( G ` y ) : ( A ^m y ) -1-1-> A <-> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) )
35 0ex 4790 . . . . . . . 8 |- (/) e. _V
36 fseqenlem.b . . . . . . . 8 |- ( ph -> B e. A )
37 f1osng 6177 . . . . . . . 8 |- ( ( (/) e. _V /\ B e. A ) -> { <. (/) , B >. } : { (/) } -1-1-onto-> { B } )
3835, 36, 37sylancr 695 . . . . . . 7 |- ( ph -> { <. (/) , B >. } : { (/) } -1-1-onto-> { B } )
39 f1of1 6136 . . . . . . 7 |- ( { <. (/) , B >. } : { (/) } -1-1-onto-> { B } -> { <. (/) , B >. } : { (/) } -1-1-> { B } )
4038, 39syl 17 . . . . . 6 |- ( ph -> { <. (/) , B >. } : { (/) } -1-1-> { B } )
4136snssd 4340 . . . . . 6 |- ( ph -> { B } C_ A )
42 f1ss 6106 . . . . . 6 |- ( ( { <. (/) , B >. } : { (/) } -1-1-> { B } /\ { B } C_ A ) -> { <. (/) , B >. } : { (/) } -1-1-> A )
4340, 41, 42syl2anc 693 . . . . 5 |- ( ph -> { <. (/) , B >. } : { (/) } -1-1-> A )
44 fseqenlem.a . . . . . . . 8 |- ( ph -> A e. V )
45 map0e 7895 . . . . . . . 8 |- ( A e. V -> ( A ^m (/) ) = 1o )
4644, 45syl 17 . . . . . . 7 |- ( ph -> ( A ^m (/) ) = 1o )
47 df1o2 7572 . . . . . . 7 |- 1o = { (/) }
4846, 47syl6eq 2672 . . . . . 6 |- ( ph -> ( A ^m (/) ) = { (/) } )
49 f1eq2 6097 . . . . . 6 |- ( ( A ^m (/) ) = { (/) } -> ( { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A <-> { <. (/) , B >. } : { (/) } -1-1-> A ) )
5048, 49syl 17 . . . . 5 |- ( ph -> ( { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A <-> { <. (/) , B >. } : { (/) } -1-1-> A ) )
5143, 50mpbird 247 . . . 4 |- ( ph -> { <. (/) , B >. } : ( A ^m (/) ) -1-1-> A )
52 fseqenlem.f . . . . . . . . . . . 12 |- ( ph -> F : ( A X. A ) -1-1-onto-> A )
5352ad2antrr 762 . . . . . . . . . . 11 |- ( ( ( 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 )
54 f1of 6137 . . . . . . . . . . 11 |- ( F : ( A X. A ) -1-1-onto-> A -> F : ( A X. A ) --> A )
5553, 54syl 17 . . . . . . . . . 10 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> F : ( A X. A ) --> A )
56 f1f 6101 . . . . . . . . . . . . 13 |- ( ( G ` m ) : ( A ^m m ) -1-1-> A -> ( G ` m ) : ( A ^m m ) --> A )
5756ad2antll 765 . . . . . . . . . . . 12 |- ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` m ) : ( A ^m m ) --> A )
5857adantr 481 . . . . . . . . . . 11 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( G ` m ) : ( A ^m m ) --> A )
59 elmapi 7879 . . . . . . . . . . . . . 14 |- ( z e. ( A ^m suc m ) -> z : suc m --> A )
6059adantl 482 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> z : suc m --> A )
61 sssucid 5802 . . . . . . . . . . . . 13 |- m C_ suc m
62 fssres 6070 . . . . . . . . . . . . 13 |- ( ( z : suc m --> A /\ m C_ suc m ) -> ( z |` m ) : m --> A )
6360, 61, 62sylancl 694 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( z |` m ) : m --> A )
6444ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> A e. V )
65 vex 3203 . . . . . . . . . . . . 13 |- m e. _V
66 elmapg 7870 . . . . . . . . . . . . 13 |- ( ( A e. V /\ m e. _V ) -> ( ( z |` m ) e. ( A ^m m ) <-> ( z |` m ) : m --> A ) )
6764, 65, 66sylancl 694 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
6863, 67mpbird 247 . . . . . . . . . . 11 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( z |` m ) e. ( A ^m m ) )
6958, 68ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( ( G ` m ) ` ( z |` m ) ) e. A )
7065sucid 5804 . . . . . . . . . . 11 |- m e. suc m
71 ffvelrn 6357 . . . . . . . . . . 11 |- ( ( z : suc m --> A /\ m e. suc m ) -> ( z ` m ) e. A )
7260, 70, 71sylancl 694 . . . . . . . . . 10 |- ( ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) /\ z e. ( A ^m suc m ) ) -> ( z ` m ) e. A )
7355, 69, 72fovrnd 6806 . . . . . . . . 9 |- ( ( ( 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 )
74 eqid 2622 . . . . . . . . 9 |- ( 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 ) ) )
7573, 74fmptd 6385 . . . . . . . 8 |- ( ( 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 ) ) ) : ( A ^m suc m ) --> A )
7611seqomsuc 7552 . . . . . . . . . . 11 |- ( 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 ) ) )
7776ad2antrl 764 . . . . . . . . . 10 |- ( ( 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 ) ) )
78 fvex 6201 . . . . . . . . . . 11 |- ( G ` m ) e. _V
79 reseq1 5390 . . . . . . . . . . . . . . . 16 |- ( x = z -> ( x |` a ) = ( z |` a ) )
8079fveq2d 6195 . . . . . . . . . . . . . . 15 |- ( x = z -> ( b ` ( x |` a ) ) = ( b ` ( z |` a ) ) )
81 fveq1 6190 . . . . . . . . . . . . . . 15 |- ( x = z -> ( x ` a ) = ( z ` a ) )
8280, 81oveq12d 6668 . . . . . . . . . . . . . 14 |- ( x = z -> ( ( b ` ( x |` a ) ) F ( x ` a ) ) = ( ( b ` ( z |` a ) ) F ( z ` a ) ) )
8382cbvmptv 4750 . . . . . . . . . . . . 13 |- ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) ) = ( z e. ( A ^m suc a ) |-> ( ( b ` ( z |` a ) ) F ( z ` a ) ) )
84 suceq 5790 . . . . . . . . . . . . . . . 16 |- ( a = m -> suc a = suc m )
8584adantr 481 . . . . . . . . . . . . . . 15 |- ( ( a = m /\ b = ( G ` m ) ) -> suc a = suc m )
8685oveq2d 6666 . . . . . . . . . . . . . 14 |- ( ( a = m /\ b = ( G ` m ) ) -> ( A ^m suc a ) = ( A ^m suc m ) )
87 simpr 477 . . . . . . . . . . . . . . . 16 |- ( ( a = m /\ b = ( G ` m ) ) -> b = ( G ` m ) )
88 reseq2 5391 . . . . . . . . . . . . . . . . 17 |- ( a = m -> ( z |` a ) = ( z |` m ) )
8988adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( a = m /\ b = ( G ` m ) ) -> ( z |` a ) = ( z |` m ) )
9087, 89fveq12d 6197 . . . . . . . . . . . . . . 15 |- ( ( a = m /\ b = ( G ` m ) ) -> ( b ` ( z |` a ) ) = ( ( G ` m ) ` ( z |` m ) ) )
91 simpl 473 . . . . . . . . . . . . . . . 16 |- ( ( a = m /\ b = ( G ` m ) ) -> a = m )
9291fveq2d 6195 . . . . . . . . . . . . . . 15 |- ( ( a = m /\ b = ( G ` m ) ) -> ( z ` a ) = ( z ` m ) )
9390, 92oveq12d 6668 . . . . . . . . . . . . . 14 |- ( ( a = m /\ b = ( G ` m ) ) -> ( ( b ` ( z |` a ) ) F ( z ` a ) ) = ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) )
9486, 93mpteq12dv 4733 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
9583, 94syl5eq 2668 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
96 nfcv 2764 . . . . . . . . . . . . 13 |- F/_ a ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) )
97 nfcv 2764 . . . . . . . . . . . . 13 |- F/_ b ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) )
98 nfcv 2764 . . . . . . . . . . . . 13 |- F/_ n ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) )
99 nfcv 2764 . . . . . . . . . . . . 13 |- F/_ f ( x e. ( A ^m suc a ) |-> ( ( b ` ( x |` a ) ) F ( x ` a ) ) )
100 suceq 5790 . . . . . . . . . . . . . . . 16 |- ( n = a -> suc n = suc a )
101100adantr 481 . . . . . . . . . . . . . . 15 |- ( ( n = a /\ f = b ) -> suc n = suc a )
102101oveq2d 6666 . . . . . . . . . . . . . 14 |- ( ( n = a /\ f = b ) -> ( A ^m suc n ) = ( A ^m suc a ) )
103 simpr 477 . . . . . . . . . . . . . . . 16 |- ( ( n = a /\ f = b ) -> f = b )
104 reseq2 5391 . . . . . . . . . . . . . . . . 17 |- ( n = a -> ( x |` n ) = ( x |` a ) )
105104adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( n = a /\ f = b ) -> ( x |` n ) = ( x |` a ) )
106103, 105fveq12d 6197 . . . . . . . . . . . . . . 15 |- ( ( n = a /\ f = b ) -> ( f ` ( x |` n ) ) = ( b ` ( x |` a ) ) )
107 simpl 473 . . . . . . . . . . . . . . . 16 |- ( ( n = a /\ f = b ) -> n = a )
108107fveq2d 6195 . . . . . . . . . . . . . . 15 |- ( ( n = a /\ f = b ) -> ( x ` n ) = ( x ` a ) )
109106, 108oveq12d 6668 . . . . . . . . . . . . . 14 |- ( ( n = a /\ f = b ) -> ( ( f ` ( x |` n ) ) F ( x ` n ) ) = ( ( b ` ( x |` a ) ) F ( x ` a ) ) )
110102, 109mpteq12dv 4733 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
11196, 97, 98, 99, 110cbvmpt2 6734 . . . . . . . . . . . 12 |- ( 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 ) ) ) )
112 ovex 6678 . . . . . . . . . . . . 13 |- ( A ^m suc m ) e. _V
113112mptex 6486 . . . . . . . . . . . 12 |- ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) e. _V
11495, 111, 113ovmpt2a 6791 . . . . . . . . . . 11 |- ( ( 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 ) ) ) )
11565, 78, 114mp2an 708 . . . . . . . . . 10 |- ( 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 ) ) )
11677, 115syl6eq 2672 . . . . . . . . 9 |- ( ( 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 ) ) ) )
117116feq1d 6030 . . . . . . . 8 |- ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( ( G ` suc m ) : ( A ^m suc m ) --> A <-> ( z e. ( A ^m suc m ) |-> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) ) : ( A ^m suc m ) --> A ) )
11875, 117mpbird 247 . . . . . . 7 |- ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` suc m ) : ( A ^m suc m ) --> A )
119 elmapi 7879 . . . . . . . . . . . . . 14 |- ( a e. ( A ^m suc m ) -> a : suc m --> A )
120119ad2antrl 764 . . . . . . . . . . . . 13 |- ( ( ( 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 )
121 ffn 6045 . . . . . . . . . . . . 13 |- ( a : suc m --> A -> a Fn suc m )
122120, 121syl 17 . . . . . . . . . . . 12 |- ( ( ( 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 )
123 elmapi 7879 . . . . . . . . . . . . . 14 |- ( b e. ( A ^m suc m ) -> b : suc m --> A )
124123ad2antll 765 . . . . . . . . . . . . 13 |- ( ( ( 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 )
125 ffn 6045 . . . . . . . . . . . . 13 |- ( b : suc m --> A -> b Fn suc m )
126124, 125syl 17 . . . . . . . . . . . 12 |- ( ( ( 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 )
12761a1i 11 . . . . . . . . . . . 12 |- ( ( ( 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 )
128 fvreseq 6319 . . . . . . . . . . . 12 |- ( ( ( a Fn suc m /\ b Fn suc m ) /\ m C_ suc m ) -> ( ( a |` m ) = ( b |` m ) <-> A. x e. m ( a ` x ) = ( b ` x ) ) )
129122, 126, 127, 128syl21anc 1325 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
130 fveq2 6191 . . . . . . . . . . . . . . 15 |- ( x = m -> ( a ` x ) = ( a ` m ) )
131 fveq2 6191 . . . . . . . . . . . . . . 15 |- ( x = m -> ( b ` x ) = ( b ` m ) )
132130, 131eqeq12d 2637 . . . . . . . . . . . . . 14 |- ( x = m -> ( ( a ` x ) = ( b ` x ) <-> ( a ` m ) = ( b ` m ) ) )
13365, 132ralsn 4222 . . . . . . . . . . . . 13 |- ( A. x e. { m } ( a ` x ) = ( b ` x ) <-> ( a ` m ) = ( b ` m ) )
134133bicomi 214 . . . . . . . . . . . 12 |- ( ( a ` m ) = ( b ` m ) <-> A. x e. { m } ( a ` x ) = ( b ` x ) )
135134a1i 11 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
136129, 135anbi12d 747 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
137116adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
138137fveq1d 6193 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
139 reseq1 5390 . . . . . . . . . . . . . . . . . 18 |- ( z = a -> ( z |` m ) = ( a |` m ) )
140139fveq2d 6195 . . . . . . . . . . . . . . . . 17 |- ( z = a -> ( ( G ` m ) ` ( z |` m ) ) = ( ( G ` m ) ` ( a |` m ) ) )
141 fveq1 6190 . . . . . . . . . . . . . . . . 17 |- ( z = a -> ( z ` m ) = ( a ` m ) )
142140, 141oveq12d 6668 . . . . . . . . . . . . . . . 16 |- ( z = a -> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) = ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) )
143 ovex 6678 . . . . . . . . . . . . . . . 16 |- ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) e. _V
144142, 74, 143fvmpt 6282 . . . . . . . . . . . . . . 15 |- ( 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 ) ) )
145144ad2antrl 764 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
146138, 145eqtrd 2656 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
147 df-ov 6653 . . . . . . . . . . . . 13 |- ( ( ( G ` m ) ` ( a |` m ) ) F ( a ` m ) ) = ( F ` <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. )
148146, 147syl6eq 2672 . . . . . . . . . . . 12 |- ( ( ( 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 ) >. ) )
149137fveq1d 6193 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
150 reseq1 5390 . . . . . . . . . . . . . . . . . 18 |- ( z = b -> ( z |` m ) = ( b |` m ) )
151150fveq2d 6195 . . . . . . . . . . . . . . . . 17 |- ( z = b -> ( ( G ` m ) ` ( z |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) )
152 fveq1 6190 . . . . . . . . . . . . . . . . 17 |- ( z = b -> ( z ` m ) = ( b ` m ) )
153151, 152oveq12d 6668 . . . . . . . . . . . . . . . 16 |- ( z = b -> ( ( ( G ` m ) ` ( z |` m ) ) F ( z ` m ) ) = ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) )
154 ovex 6678 . . . . . . . . . . . . . . . 16 |- ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) e. _V
155153, 74, 154fvmpt 6282 . . . . . . . . . . . . . . 15 |- ( 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 ) ) )
156155ad2antll 765 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
157149, 156eqtrd 2656 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
158 df-ov 6653 . . . . . . . . . . . . 13 |- ( ( ( G ` m ) ` ( b |` m ) ) F ( b ` m ) ) = ( F ` <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. )
159157, 158syl6eq 2672 . . . . . . . . . . . 12 |- ( ( ( 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 ) >. ) )
160148, 159eqeq12d 2637 . . . . . . . . . . 11 |- ( ( ( 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 ) >. ) ) )
16152ad2antrr 762 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
162 f1of1 6136 . . . . . . . . . . . . . 14 |- ( F : ( A X. A ) -1-1-onto-> A -> F : ( A X. A ) -1-1-> A )
163161, 162syl 17 . . . . . . . . . . . . 13 |- ( ( ( 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 )
16457adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( 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 )
165 fssres 6070 . . . . . . . . . . . . . . . . 17 |- ( ( a : suc m --> A /\ m C_ suc m ) -> ( a |` m ) : m --> A )
166120, 61, 165sylancl 694 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 )
16744ad2antrr 762 . . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
168 elmapg 7870 . . . . . . . . . . . . . . . . 17 |- ( ( A e. V /\ m e. _V ) -> ( ( a |` m ) e. ( A ^m m ) <-> ( a |` m ) : m --> A ) )
169167, 65, 168sylancl 694 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) )
170166, 169mpbird 247 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
171164, 170ffvelrnd 6360 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
172 ffvelrn 6357 . . . . . . . . . . . . . . 15 |- ( ( a : suc m --> A /\ m e. suc m ) -> ( a ` m ) e. A )
173120, 70, 172sylancl 694 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
174 opelxpi 5148 . . . . . . . . . . . . . 14 |- ( ( ( ( G ` m ) ` ( a |` m ) ) e. A /\ ( a ` m ) e. A ) -> <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. e. ( A X. A ) )
175171, 173, 174syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
176 fssres 6070 . . . . . . . . . . . . . . . . 17 |- ( ( b : suc m --> A /\ m C_ suc m ) -> ( b |` m ) : m --> A )
177124, 61, 176sylancl 694 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 )
178 elmapg 7870 . . . . . . . . . . . . . . . . 17 |- ( ( A e. V /\ m e. _V ) -> ( ( b |` m ) e. ( A ^m m ) <-> ( b |` m ) : m --> A ) )
179167, 65, 178sylancl 694 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) )
180177, 179mpbird 247 . . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
181164, 180ffvelrnd 6360 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
182 ffvelrn 6357 . . . . . . . . . . . . . . 15 |- ( ( b : suc m --> A /\ m e. suc m ) -> ( b ` m ) e. A )
183124, 70, 182sylancl 694 . . . . . . . . . . . . . 14 |- ( ( ( 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 )
184 opelxpi 5148 . . . . . . . . . . . . . 14 |- ( ( ( ( G ` m ) ` ( b |` m ) ) e. A /\ ( b ` m ) e. A ) -> <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. e. ( A X. A ) )
185181, 183, 184syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( 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 ) )
186 f1fveq 6519 . . . . . . . . . . . . 13 |- ( ( 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 ) >. ) )
187163, 175, 185, 186syl12anc 1324 . . . . . . . . . . . 12 |- ( ( ( 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 ) >. ) )
188 fvex 6201 . . . . . . . . . . . . 13 |- ( ( G ` m ) ` ( a |` m ) ) e. _V
189 fvex 6201 . . . . . . . . . . . . 13 |- ( a ` m ) e. _V
190188, 189opth 4945 . . . . . . . . . . . 12 |- ( <. ( ( G ` m ) ` ( a |` m ) ) , ( a ` m ) >. = <. ( ( G ` m ) ` ( b |` m ) ) , ( b ` m ) >. <-> ( ( ( G ` m ) ` ( a |` m ) ) = ( ( G ` m ) ` ( b |` m ) ) /\ ( a ` m ) = ( b ` m ) ) )
191187, 190syl6bb 276 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
192 simplrr 801 . . . . . . . . . . . . 13 |- ( ( ( 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 )
193 f1fveq 6519 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
194192, 170, 180, 193syl12anc 1324 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
195194anbi1d 741 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
196160, 191, 1953bitrd 294 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
197 eqfnfv 6311 . . . . . . . . . . . 12 |- ( ( a Fn suc m /\ b Fn suc m ) -> ( a = b <-> A. x e. suc m ( a ` x ) = ( b ` x ) ) )
198122, 126, 197syl2anc 693 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
199 df-suc 5729 . . . . . . . . . . . . 13 |- suc m = ( m u. { m } )
200199raleqi 3142 . . . . . . . . . . . 12 |- ( A. x e. suc m ( a ` x ) = ( b ` x ) <-> A. x e. ( m u. { m } ) ( a ` x ) = ( b ` x ) )
201 ralunb 3794 . . . . . . . . . . . 12 |- ( 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 ) ) )
202200, 201bitri 264 . . . . . . . . . . 11 |- ( 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 ) ) )
203198, 202syl6bb 276 . . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
204136, 196, 2033bitr4d 300 . . . . . . . . 9 |- ( ( ( 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 ) )
205204biimpd 219 . . . . . . . 8 |- ( ( ( 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 ) )
206205ralrimivva 2971 . . . . . . 7 |- ( ( 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 ) )
207 dff13 6512 . . . . . . 7 |- ( ( 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 ) ) )
208118, 206, 207sylanbrc 698 . . . . . 6 |- ( ( ph /\ ( m e. om /\ ( G ` m ) : ( A ^m m ) -1-1-> A ) ) -> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A )
209208expr 643 . . . . 5 |- ( ( ph /\ m e. om ) -> ( ( G ` m ) : ( A ^m m ) -1-1-> A -> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) )
210209expcom 451 . . . 4 |- ( m e. om -> ( ph -> ( ( G ` m ) : ( A ^m m ) -1-1-> A -> ( G ` suc m ) : ( A ^m suc m ) -1-1-> A ) ) )
21120, 27, 34, 51, 210finds2 7094 . . 3 |- ( y e. om -> ( ph -> ( G ` y ) : ( A ^m y ) -1-1-> A ) )
2128, 211vtoclga 3272 . 2 |- ( C e. om -> ( ph -> ( G ` C ) : ( A ^m C ) -1-1-> A ) )
213212impcom 446 1 |- ( ( ph /\ C e. om ) -> ( G ` C ) : ( A ^m C ) -1-1-> A )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   u. cun 3572   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   |-> cmpt 4729   X. cxp 5112   |` cres 5116   suc csuc 5725   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   omcom 7065  seq𝜔cseqom 7542   1oc1o 7553   ^m cmap 7857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seqom 7543  df-1o 7560  df-map 7859
This theorem is referenced by:  fseqenlem2  8848
  Copyright terms: Public domain W3C validator