Theorem fseqenlem2 8848

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 >. } )
fseqenlem.k	|- K = ( y e. U_ k e. om ( A ^m k ) |-> <. dom y , ( ( G ` dom y ) ` y ) >. )

Assertion

Ref	Expression
fseqenlem2	|- ( ph -> K : U_ k e. om ( A ^m k ) -1-1-> ( om X. A ) )

Distinct variable groups:   y, B   f, n, x, F   y, k, G   f, k, y, A, n, x   ph, k, n, x, y

Allowed substitution hints:   ph( f)   B( x, f, k, n)   F( y, k)   G( x, f, n)   K( x, y, f, k, n)   V( x, y, f, k, n)

Proof of Theorem fseqenlem2

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eliun 4524	. . . . 5 |- ( y e. U_ k e. om ( A ^m k ) <-> E. k e. om y e. ( A ^m k ) )
2		elmapi 7879	. . . . . . . . . 10 |- ( y e. ( A ^m k ) -> y : k --> A )
3	2	ad2antll 765	. . . . . . . . 9 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> y : k --> A )
4		fdm 6051	. . . . . . . . 9 |- ( y : k --> A -> dom y = k )
5	3, 4	syl 17	. . . . . . . 8 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> dom y = k )
6		simprl 794	. . . . . . . 8 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> k e. om )
7	5, 6	eqeltrd 2701	. . . . . . 7 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> dom y e. om )
8	5	fveq2d 6195	. . . . . . . . 9 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> ( G ` dom y ) = ( G ` k ) )
9	8	fveq1d 6193	. . . . . . . 8 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> ( ( G ` dom y ) ` y ) = ( ( G ` k ) ` y ) )
10		fseqenlem.a	. . . . . . . . . . . 12 |- ( ph -> A e. V )
11		fseqenlem.b	. . . . . . . . . . . 12 |- ( ph -> B e. A )
12		fseqenlem.f	. . . . . . . . . . . 12 |- ( ph -> F : ( A X. A ) -1-1-onto-> A )
13		fseqenlem.g	. . . . . . . . . . . 12 |- G = seq𝜔 ( ( n e. _V , f e. _V |-> ( x e. ( A ^m suc n ) |-> ( ( f ` ( x |` n ) ) F ( x ` n ) ) ) ) , { <. (/) , B >. } )
14	10, 11, 12, 13	fseqenlem1 8847	. . . . . . . . . . 11 |- ( ( ph /\ k e. om ) -> ( G ` k ) : ( A ^m k ) -1-1-> A )
15	14	adantrr 753	. . . . . . . . . 10 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> ( G ` k ) : ( A ^m k ) -1-1-> A )
16		f1f 6101	. . . . . . . . . 10 |- ( ( G ` k ) : ( A ^m k ) -1-1-> A -> ( G ` k ) : ( A ^m k ) --> A )
17	15, 16	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> ( G ` k ) : ( A ^m k ) --> A )
18		simprr 796	. . . . . . . . 9 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> y e. ( A ^m k ) )
19	17, 18	ffvelrnd 6360	. . . . . . . 8 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> ( ( G ` k ) ` y ) e. A )
20	9, 19	eqeltrd 2701	. . . . . . 7 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> ( ( G ` dom y ) ` y ) e. A )
21		opelxpi 5148	. . . . . . 7 |- ( ( dom y e. om /\ ( ( G ` dom y ) ` y ) e. A ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( om X. A ) )
22	7, 20, 21	syl2anc 693	. . . . . 6 |- ( ( ph /\ ( k e. om /\ y e. ( A ^m k ) ) ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( om X. A ) )
23	22	rexlimdvaa 3032	. . . . 5 |- ( ph -> ( E. k e. om y e. ( A ^m k ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( om X. A ) ) )
24	1, 23	syl5bi 232	. . . 4 |- ( ph -> ( y e. U_ k e. om ( A ^m k ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( om X. A ) ) )
25	24	imp 445	. . 3 |- ( ( ph /\ y e. U_ k e. om ( A ^m k ) ) -> <. dom y , ( ( G ` dom y ) ` y ) >. e. ( om X. A ) )
26		fseqenlem.k	. . 3 |- K = ( y e. U_ k e. om ( A ^m k ) |-> <. dom y , ( ( G ` dom y ) ` y ) >. )
27	25, 26	fmptd 6385	. 2 |- ( ph -> K : U_ k e. om ( A ^m k ) --> ( om X. A ) )
28		ffun 6048	. . . . . . . . . . . . . . 15 |- ( K : U_ k e. om ( A ^m k ) --> ( om X. A ) -> Fun K )
29		funbrfv2b 6240	. . . . . . . . . . . . . . 15 |- ( Fun K -> ( z K w <-> ( z e. dom K /\ ( K ` z ) = w ) ) )
30	27, 28, 29	3syl 18	. . . . . . . . . . . . . 14 |- ( ph -> ( z K w <-> ( z e. dom K /\ ( K ` z ) = w ) ) )
31	30	simplbda 654	. . . . . . . . . . . . 13 |- ( ( ph /\ z K w ) -> ( K ` z ) = w )
32	30	simprbda 653	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z K w ) -> z e. dom K )
33		fdm 6051	. . . . . . . . . . . . . . . . 17 |- ( K : U_ k e. om ( A ^m k ) --> ( om X. A ) -> dom K = U_ k e. om ( A ^m k ) )
34	27, 33	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom K = U_ k e. om ( A ^m k ) )
35	34	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z K w ) -> dom K = U_ k e. om ( A ^m k ) )
36	32, 35	eleqtrd 2703	. . . . . . . . . . . . . 14 |- ( ( ph /\ z K w ) -> z e. U_ k e. om ( A ^m k ) )
37		dmeq 5324	. . . . . . . . . . . . . . . 16 |- ( y = z -> dom y = dom z )
38	37	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( y = z -> ( G ` dom y ) = ( G ` dom z ) )
39		id 22	. . . . . . . . . . . . . . . . 17 |- ( y = z -> y = z )
40	38, 39	fveq12d 6197	. . . . . . . . . . . . . . . 16 |- ( y = z -> ( ( G ` dom y ) ` y ) = ( ( G ` dom z ) ` z ) )
41	37, 40	opeq12d 4410	. . . . . . . . . . . . . . 15 |- ( y = z -> <. dom y , ( ( G ` dom y ) ` y ) >. = <. dom z , ( ( G ` dom z ) ` z ) >. )
42		opex 4932	. . . . . . . . . . . . . . 15 |- <. dom z , ( ( G ` dom z ) ` z ) >. e. _V
43	41, 26, 42	fvmpt 6282	. . . . . . . . . . . . . 14 |- ( z e. U_ k e. om ( A ^m k ) -> ( K ` z ) = <. dom z , ( ( G ` dom z ) ` z ) >. )
44	36, 43	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ z K w ) -> ( K ` z ) = <. dom z , ( ( G ` dom z ) ` z ) >. )
45	31, 44	eqtr3d 2658	. . . . . . . . . . . 12 |- ( ( ph /\ z K w ) -> w = <. dom z , ( ( G ` dom z ) ` z ) >. )
46	45	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ph /\ z K w ) -> ( 1st ` w ) = ( 1st ` <. dom z , ( ( G ` dom z ) ` z ) >. ) )
47		vex 3203	. . . . . . . . . . . . 13 |- z e. _V
48	47	dmex 7099	. . . . . . . . . . . 12 |- dom z e. _V
49		fvex 6201	. . . . . . . . . . . 12 |- ( ( G ` dom z ) ` z ) e. _V
50	48, 49	op1st 7176	. . . . . . . . . . 11 |- ( 1st ` <. dom z , ( ( G ` dom z ) ` z ) >. ) = dom z
51	46, 50	syl6eq 2672	. . . . . . . . . 10 |- ( ( ph /\ z K w ) -> ( 1st ` w ) = dom z )
52	51	fveq2d 6195	. . . . . . . . 9 |- ( ( ph /\ z K w ) -> ( G ` ( 1st ` w ) ) = ( G ` dom z ) )
53	52	cnveqd 5298	. . . . . . . 8 |- ( ( ph /\ z K w ) -> `' ( G ` ( 1st ` w ) ) = `' ( G ` dom z ) )
54	45	fveq2d 6195	. . . . . . . . 9 |- ( ( ph /\ z K w ) -> ( 2nd ` w ) = ( 2nd ` <. dom z , ( ( G ` dom z ) ` z ) >. ) )
55	48, 49	op2nd 7177	. . . . . . . . 9 |- ( 2nd ` <. dom z , ( ( G ` dom z ) ` z ) >. ) = ( ( G ` dom z ) ` z )
56	54, 55	syl6eq 2672	. . . . . . . 8 |- ( ( ph /\ z K w ) -> ( 2nd ` w ) = ( ( G ` dom z ) ` z ) )
57	53, 56	fveq12d 6197	. . . . . . 7 |- ( ( ph /\ z K w ) -> ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) = ( `' ( G ` dom z ) ` ( ( G ` dom z ) ` z ) ) )
58		eliun 4524	. . . . . . . . . . . . 13 |- ( z e. U_ k e. om ( A ^m k ) <-> E. k e. om z e. ( A ^m k ) )
59		elmapi 7879	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( A ^m k ) -> z : k --> A )
60	59	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> z : k --> A )
61		fdm 6051	. . . . . . . . . . . . . . . . 17 |- ( z : k --> A -> dom z = k )
62	60, 61	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> dom z = k )
63		simpl 473	. . . . . . . . . . . . . . . 16 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> k e. om )
64	62, 63	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> dom z e. om )
65		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> z e. ( A ^m k ) )
66	62	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> ( A ^m dom z ) = ( A ^m k ) )
67	65, 66	eleqtrrd 2704	. . . . . . . . . . . . . . 15 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> z e. ( A ^m dom z ) )
68	64, 67	jca 554	. . . . . . . . . . . . . 14 |- ( ( k e. om /\ z e. ( A ^m k ) ) -> ( dom z e. om /\ z e. ( A ^m dom z ) ) )
69	68	rexlimiva 3028	. . . . . . . . . . . . 13 |- ( E. k e. om z e. ( A ^m k ) -> ( dom z e. om /\ z e. ( A ^m dom z ) ) )
70	58, 69	sylbi 207	. . . . . . . . . . . 12 |- ( z e. U_ k e. om ( A ^m k ) -> ( dom z e. om /\ z e. ( A ^m dom z ) ) )
71	36, 70	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ z K w ) -> ( dom z e. om /\ z e. ( A ^m dom z ) ) )
72	71	simpld 475	. . . . . . . . . 10 |- ( ( ph /\ z K w ) -> dom z e. om )
73	10, 11, 12, 13	fseqenlem1 8847	. . . . . . . . . 10 |- ( ( ph /\ dom z e. om ) -> ( G ` dom z ) : ( A ^m dom z ) -1-1-> A )
74	72, 73	syldan 487	. . . . . . . . 9 |- ( ( ph /\ z K w ) -> ( G ` dom z ) : ( A ^m dom z ) -1-1-> A )
75		f1f1orn 6148	. . . . . . . . 9 |- ( ( G ` dom z ) : ( A ^m dom z ) -1-1-> A -> ( G ` dom z ) : ( A ^m dom z ) -1-1-onto-> ran ( G ` dom z ) )
76	74, 75	syl 17	. . . . . . . 8 |- ( ( ph /\ z K w ) -> ( G ` dom z ) : ( A ^m dom z ) -1-1-onto-> ran ( G ` dom z ) )
77	71	simprd 479	. . . . . . . 8 |- ( ( ph /\ z K w ) -> z e. ( A ^m dom z ) )
78		f1ocnvfv1 6532	. . . . . . . 8 |- ( ( ( 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 )
79	76, 77, 78	syl2anc 693	. . . . . . 7 |- ( ( ph /\ z K w ) -> ( `' ( G ` dom z ) ` ( ( G ` dom z ) ` z ) ) = z )
80	57, 79	eqtr2d 2657	. . . . . 6 |- ( ( ph /\ z K w ) -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) )
81	80	ex 450	. . . . 5 |- ( ph -> ( z K w -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) ) )
82	81	alrimiv 1855	. . . 4 |- ( ph -> A. z ( z K w -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) ) )
83		mo2icl 3385	. . . 4 |- ( A. z ( z K w -> z = ( `' ( G ` ( 1st ` w ) ) ` ( 2nd ` w ) ) ) -> E* z z K w )
84	82, 83	syl 17	. . 3 |- ( ph -> E* z z K w )
85	84	alrimiv 1855	. 2 |- ( ph -> A. w E* z z K w )
86		dff12 6100	. 2 |- ( 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 ) )
87	27, 85, 86	sylanbrc 698	1 |- ( ph -> K : U_ k e. om ( A ^m k ) -1-1-> ( om X. A ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   E*wmo 2471   E.wrex 2913   _Vcvv 3200   (/)c0 3915   {csn 4177   <.cop 4183   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   |` cres 5116   suc csuc 5725   Fun wfun 5882   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   omcom 7065   1stc1st 7166   2ndc2nd 7167  seq_𝜔cseqom 7542   ^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:  fseqen  8850  pwfseqlem5  9485