Metamath Proof Explorer

Theorem fseqenlem2

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 >. } )
fseqenlem.k 
|- K = ( y e. U_ k e. _om ( A ^m k ) |-> <. dom y , ( ( G ` dom y ) ` y ) >. )
Assertion fseqenlem2 
|- ( ph -> K : U_ k e. _om ( A ^m k ) -1-1-> ( _om X. 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 fseqenlem.k 
 |-  K = ( y e. U_ k e. _om ( A ^m k ) |-> <. dom y , ( ( G ` dom y ) ` y ) >. )
6 eliun 
 |-  ( y e. U_ k e. _om ( A ^m k ) <-> E. k e. _om y e. ( A ^m k ) )
7 elmapi 
 |-  ( y e. ( A ^m k ) -> y : k --> A )
8 7 ad2antll 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> y : k --> A )
9 8 fdmd 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> dom y = k )
10 simprl 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> k e. _om )
11 9 10 eqeltrd 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> dom y e. _om )
12 9 fveq2d 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> ( G ` dom y ) = ( G ` k ) )
13 12 fveq1d 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> ( ( G ` dom y ) ` y ) = ( ( G ` k ) ` y ) )
14 1 2 3 4 fseqenlem1 
 |-  ( ( ph /\ k e. _om ) -> ( G ` k ) : ( A ^m k ) -1-1-> A )
15 14 adantrr 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> ( G ` k ) : ( A ^m k ) -1-1-> A )
16 f1f 
 |-  ( ( G ` k ) : ( A ^m k ) -1-1-> A -> ( G ` k ) : ( A ^m k ) --> A )
17 15 16 syl 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> ( G ` k ) : ( A ^m k ) --> A )
18 simprr 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> y e. ( A ^m k ) )
19 17 18 ffvelrnd 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> ( ( G ` k ) ` y ) e. A )
20 13 19 eqeltrd 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> ( ( G ` dom y ) ` y ) e. A )
21 11 20 opelxpd 
 |-  ( ( ph /\ ( k e. _om /\ y e. ( A ^m k ) ) ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( _om X. A ) )
22 21 rexlimdvaa 
 |-  ( ph -> ( E. k e. _om y e. ( A ^m k ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( _om X. A ) ) )
23 6 22 syl5bi 
 |-  ( ph -> ( y e. U_ k e. _om ( A ^m k ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( _om X. A ) ) )
24 23 imp 
 |-  ( ( ph /\ y e. U_ k e. _om ( A ^m k ) ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( _om X. A ) )
25 24 5 fmptd 
 |-  ( ph -> K : U_ k e. _om ( A ^m k ) --> ( _om X. A ) )
26 ffun 
 |-  ( K : U_ k e. _om ( A ^m k ) --> ( _om X. A ) -> Fun K )
27 funbrfv2b 
 |-  ( Fun K -> ( z K w <-> ( z e. dom K /\ ( K ` z ) = w ) ) )
28 25 26 27 3syl 
 |-  ( ph -> ( z K w <-> ( z e. dom K /\ ( K ` z ) = w ) ) )
29 28 simplbda 
 |-  ( ( ph /\ z K w ) -> ( K ` z ) = w )
30 28 simprbda 
 |-  ( ( ph /\ z K w ) -> z e. dom K )
31 25 fdmd 
 |-  ( ph -> dom K = U_ k e. _om ( A ^m k ) )
32 31 adantr 
 |-  ( ( ph /\ z K w ) -> dom K = U_ k e. _om ( A ^m k ) )
33 30 32 eleqtrd 
 |-  ( ( ph /\ z K w ) -> z e. U_ k e. _om ( A ^m k ) )
34 dmeq 
 |-  ( y = z -> dom y = dom z )
35 34 fveq2d 
 |-  ( y = z -> ( G ` dom y ) = ( G ` dom z ) )
36 id 
 |-  ( y = z -> y = z )
37 35 36 fveq12d 
 |-  ( y = z -> ( ( G ` dom y ) ` y ) = ( ( G ` dom z ) ` z ) )
38 34 37 opeq12d 
 |-  ( y = z -> <. dom y , ( ( G ` dom y ) ` y ) >. = <. dom z , ( ( G ` dom z ) ` z ) >. )
39 opex 
 |-  <. dom z , ( ( G ` dom z ) ` z ) >. e. _V
40 38 5 39 fvmpt 
 |-  ( z e. U_ k e. _om ( A ^m k ) -> ( K ` z ) = <. dom z , ( ( G ` dom z ) ` z ) >. )
41 33 40 syl 
 |-  ( ( ph /\ z K w ) -> ( K ` z ) = <. dom z , ( ( G ` dom z ) ` z ) >. )
42 29 41 eqtr3d 
 |-  ( ( ph /\ z K w ) -> w = <. dom z , ( ( G ` dom z ) ` z ) >. )
43 42 fveq2d 
 |-  ( ( ph /\ z K w ) -> ( 1st ` w ) = ( 1st ` <. dom z , ( ( G ` dom z ) ` z ) >. ) )
44 vex 
 |-  z e. _V
45 44 dmex 
 |-  dom z e. _V
46 fvex 
 |-  ( ( G ` dom z ) ` z ) e. _V
47 45 46 op1st 
 |-  ( 1st ` <. dom z , ( ( G ` dom z ) ` z ) >. ) = dom z
48 43 47 eqtrdi 
 |-  ( ( ph /\ z K w ) -> ( 1st ` w ) = dom z )
49 48 fveq2d 
 |-  ( ( ph /\ z K w ) -> ( G ` ( 1st ` w ) ) = ( G ` dom z ) )
50 49 cnveqd 
 |-  ( ( ph /\ z K w ) -> `' ( G ` ( 1st ` w ) ) = `' ( G ` dom z ) )
51 42 fveq2d 
 |-  ( ( ph /\ z K w ) -> ( 2nd ` w ) = ( 2nd ` <. dom z , ( ( G ` dom z ) ` z ) >. ) )
52 45 46 op2nd 
 |-  ( 2nd ` <. dom z , ( ( G ` dom z ) ` z ) >. ) = ( ( G ` dom z ) ` z )
53 51 52 eqtrdi 
 |-  ( ( ph /\ z K w ) -> ( 2nd ` w ) = ( ( G ` dom z ) ` z ) )
54 50 53 fveq12d 
 |-  ( ( ph /\ z K w ) -> ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) = ( `' ( G ` dom z ) ` ( ( G ` dom z ) ` z ) ) )
55 eliun 
 |-  ( z e. U_ k e. _om ( A ^m k ) <-> E. k e. _om z e. ( A ^m k ) )
56 elmapi 
 |-  ( z e. ( A ^m k ) -> z : k --> A )
57 56 adantl 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> z : k --> A )
58 57 fdmd 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> dom z = k )
59 simpl 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> k e. _om )
60 58 59 eqeltrd 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> dom z e. _om )
61 simpr 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> z e. ( A ^m k ) )
62 58 oveq2d 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> ( A ^m dom z ) = ( A ^m k ) )
63 61 62 eleqtrrd 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> z e. ( A ^m dom z ) )
64 60 63 jca 
 |-  ( ( k e. _om /\ z e. ( A ^m k ) ) -> ( dom z e. _om /\ z e. ( A ^m dom z ) ) )
65 64 rexlimiva 
 |-  ( E. k e. _om z e. ( A ^m k ) -> ( dom z e. _om /\ z e. ( A ^m dom z ) ) )
66 55 65 sylbi 
 |-  ( z e. U_ k e. _om ( A ^m k ) -> ( dom z e. _om /\ z e. ( A ^m dom z ) ) )
67 33 66 syl 
 |-  ( ( ph /\ z K w ) -> ( dom z e. _om /\ z e. ( A ^m dom z ) ) )
68 67 simpld 
 |-  ( ( ph /\ z K w ) -> dom z e. _om )
69 1 2 3 4 fseqenlem1 
 |-  ( ( ph /\ dom z e. _om ) -> ( G ` dom z ) : ( A ^m dom z ) -1-1-> A )
70 68 69 syldan 
 |-  ( ( ph /\ z K w ) -> ( G ` dom z ) : ( A ^m dom z ) -1-1-> A )
71 f1f1orn 
 |-  ( ( G ` dom z ) : ( A ^m dom z ) -1-1-> A -> ( G ` dom z ) : ( A ^m dom z ) -1-1-onto-> ran ( G ` dom z ) )
72 70 71 syl 
 |-  ( ( ph /\ z K w ) -> ( G ` dom z ) : ( A ^m dom z ) -1-1-onto-> ran ( G ` dom z ) )
73 67 simprd 
 |-  ( ( ph /\ z K w ) -> z e. ( A ^m dom z ) )
74 f1ocnvfv1 
 |-  ( ( ( G ` dom z ) : ( A ^m dom z ) -1-1-onto-> ran ( G ` dom z ) /\ z e. ( A ^m dom z ) ) -> ( `' ( G ` dom z ) ` ( ( G ` dom z ) ` z ) ) = z )
75 72 73 74 syl2anc 
 |-  ( ( ph /\ z K w ) -> ( `' ( G ` dom z ) ` ( ( G ` dom z ) ` z ) ) = z )
76 54 75 eqtr2d 
 |-  ( ( ph /\ z K w ) -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) )
77 76 ex 
 |-  ( ph -> ( z K w -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) ) )
78 77 alrimiv 
 |-  ( ph -> A. z ( z K w -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) ) )
79 mo2icl 
 |-  ( A. z ( z K w -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) ) -> E* z z K w )
80 78 79 syl 
 |-  ( ph -> E* z z K w )
81 80 alrimiv 
 |-  ( ph -> A. w E* z z K w )
82 dff12 
 |-  ( K : U_ k e. _om ( A ^m k ) -1-1-> ( _om X. A ) <-> ( K : U_ k e. _om ( A ^m k ) --> ( _om X. A ) /\ A. w E* z z K w ) )
83 25 81 82 sylanbrc 
 |-  ( ph -> K : U_ k e. _om ( A ^m k ) -1-1-> ( _om X. A ) )