fin23lem28

Description: Lemma for fin23 . The residual is also one-to-one. This preserves the induction invariant. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem.a	\|- U = seqom ( ( i e. _om , u e. _V \|-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
	fin23lem17.f	\|- F = { g \| A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> \|^\| ran a e. ran a ) }
	fin23lem.b	\|- P = { v e. _om \| \|^\| ran U C_ ( t ` v ) }
	fin23lem.c	\|- Q = ( w e. _om \|-> ( iota_ x e. P ( x i^i P ) ~~ w ) )
	fin23lem.d	\|- R = ( w e. _om \|-> ( iota_ x e. ( _om \ P ) ( x i^i ( _om \ P ) ) ~~ w ) )
	fin23lem.e	\|- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) )
Assertion	fin23lem28	\|- ( t : _om -1-1-> _V -> Z : _om -1-1-> _V )

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	\|- U = seqom ( ( i e. _om , u e. _V \|-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
2		fin23lem17.f	\|- F = { g \| A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> \|^\| ran a e. ran a ) }
3		fin23lem.b	\|- P = { v e. _om \| \|^\| ran U C_ ( t ` v ) }
4		fin23lem.c	\|- Q = ( w e. _om \|-> ( iota_ x e. P ( x i^i P ) ~~ w ) )
5		fin23lem.d	\|- R = ( w e. _om \|-> ( iota_ x e. ( _om \ P ) ( x i^i ( _om \ P ) ) ~~ w ) )
6		fin23lem.e	\|- Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) )
7		eqif	\|- ( Z = if ( P e. Fin , ( t o. R ) , ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) ) <-> ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) ) ) )
8	6 7	mpbi	\|- ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) ) )
9		difss	\|- ( _om \ P ) C_ _om
10		ominf	\|- -. _om e. Fin
11	3	ssrab3	\|- P C_ _om
12		undif	\|- ( P C_ _om <-> ( P u. ( _om \ P ) ) = _om )
13	11 12	mpbi	\|- ( P u. ( _om \ P ) ) = _om
14		unfi	\|- ( ( P e. Fin /\ ( _om \ P ) e. Fin ) -> ( P u. ( _om \ P ) ) e. Fin )
15	13 14	eqeltrrid	\|- ( ( P e. Fin /\ ( _om \ P ) e. Fin ) -> _om e. Fin )
16	15	ex	\|- ( P e. Fin -> ( ( _om \ P ) e. Fin -> _om e. Fin ) )
17	10 16	mtoi	\|- ( P e. Fin -> -. ( _om \ P ) e. Fin )
18	5	fin23lem22	\|- ( ( ( _om \ P ) C_ _om /\ -. ( _om \ P ) e. Fin ) -> R : _om -1-1-onto-> ( _om \ P ) )
19	9 17 18	sylancr	\|- ( P e. Fin -> R : _om -1-1-onto-> ( _om \ P ) )
20	19	adantl	\|- ( ( t : _om -1-1-> _V /\ P e. Fin ) -> R : _om -1-1-onto-> ( _om \ P ) )
21		f1of1	\|- ( R : _om -1-1-onto-> ( _om \ P ) -> R : _om -1-1-> ( _om \ P ) )
22		f1ss	\|- ( ( R : _om -1-1-> ( _om \ P ) /\ ( _om \ P ) C_ _om ) -> R : _om -1-1-> _om )
23	9 22	mpan2	\|- ( R : _om -1-1-> ( _om \ P ) -> R : _om -1-1-> _om )
24	20 21 23	3syl	\|- ( ( t : _om -1-1-> _V /\ P e. Fin ) -> R : _om -1-1-> _om )
25		f1co	\|- ( ( t : _om -1-1-> _V /\ R : _om -1-1-> _om ) -> ( t o. R ) : _om -1-1-> _V )
26	24 25	syldan	\|- ( ( t : _om -1-1-> _V /\ P e. Fin ) -> ( t o. R ) : _om -1-1-> _V )
27		f1eq1	\|- ( Z = ( t o. R ) -> ( Z : _om -1-1-> _V <-> ( t o. R ) : _om -1-1-> _V ) )
28	26 27	syl5ibrcom	\|- ( ( t : _om -1-1-> _V /\ P e. Fin ) -> ( Z = ( t o. R ) -> Z : _om -1-1-> _V ) )
29	28	impr	\|- ( ( t : _om -1-1-> _V /\ ( P e. Fin /\ Z = ( t o. R ) ) ) -> Z : _om -1-1-> _V )
30		fvex	\|- ( t ` z ) e. _V
31	30	difexi	\|- ( ( t ` z ) \ \|^\| ran U ) e. _V
32	31	rgenw	\|- A. z e. P ( ( t ` z ) \ \|^\| ran U ) e. _V
33		eqid	\|- ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) = ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) )
34	33	fmpt	\|- ( A. z e. P ( ( t ` z ) \ \|^\| ran U ) e. _V <-> ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) : P --> _V )
35	32 34	mpbi	\|- ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) : P --> _V
36	35	a1i	\|- ( t : _om -1-1-> _V -> ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) : P --> _V )
37		fveq2	\|- ( z = a -> ( t ` z ) = ( t ` a ) )
38	37	difeq1d	\|- ( z = a -> ( ( t ` z ) \ \|^\| ran U ) = ( ( t ` a ) \ \|^\| ran U ) )
39		fvex	\|- ( t ` a ) e. _V
40	39	difexi	\|- ( ( t ` a ) \ \|^\| ran U ) e. _V
41	38 33 40	fvmpt	\|- ( a e. P -> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` a ) = ( ( t ` a ) \ \|^\| ran U ) )
42	41	ad2antrl	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` a ) = ( ( t ` a ) \ \|^\| ran U ) )
43		fveq2	\|- ( z = b -> ( t ` z ) = ( t ` b ) )
44	43	difeq1d	\|- ( z = b -> ( ( t ` z ) \ \|^\| ran U ) = ( ( t ` b ) \ \|^\| ran U ) )
45		fvex	\|- ( t ` b ) e. _V
46	45	difexi	\|- ( ( t ` b ) \ \|^\| ran U ) e. _V
47	44 33 46	fvmpt	\|- ( b e. P -> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` b ) = ( ( t ` b ) \ \|^\| ran U ) )
48	47	ad2antll	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` b ) = ( ( t ` b ) \ \|^\| ran U ) )
49	42 48	eqeq12d	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` a ) = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` b ) <-> ( ( t ` a ) \ \|^\| ran U ) = ( ( t ` b ) \ \|^\| ran U ) ) )
50		uneq2	\|- ( ( ( t ` a ) \ \|^\| ran U ) = ( ( t ` b ) \ \|^\| ran U ) -> ( \|^\| ran U u. ( ( t ` a ) \ \|^\| ran U ) ) = ( \|^\| ran U u. ( ( t ` b ) \ \|^\| ran U ) ) )
51		fveq2	\|- ( v = a -> ( t ` v ) = ( t ` a ) )
52	51	sseq2d	\|- ( v = a -> ( \|^\| ran U C_ ( t ` v ) <-> \|^\| ran U C_ ( t ` a ) ) )
53	52 3	elrab2	\|- ( a e. P <-> ( a e. _om /\ \|^\| ran U C_ ( t ` a ) ) )
54	53	simprbi	\|- ( a e. P -> \|^\| ran U C_ ( t ` a ) )
55	54	ad2antrl	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> \|^\| ran U C_ ( t ` a ) )
56		undif	\|- ( \|^\| ran U C_ ( t ` a ) <-> ( \|^\| ran U u. ( ( t ` a ) \ \|^\| ran U ) ) = ( t ` a ) )
57	55 56	sylib	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( \|^\| ran U u. ( ( t ` a ) \ \|^\| ran U ) ) = ( t ` a ) )
58		fveq2	\|- ( v = b -> ( t ` v ) = ( t ` b ) )
59	58	sseq2d	\|- ( v = b -> ( \|^\| ran U C_ ( t ` v ) <-> \|^\| ran U C_ ( t ` b ) ) )
60	59 3	elrab2	\|- ( b e. P <-> ( b e. _om /\ \|^\| ran U C_ ( t ` b ) ) )
61	60	simprbi	\|- ( b e. P -> \|^\| ran U C_ ( t ` b ) )
62	61	ad2antll	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> \|^\| ran U C_ ( t ` b ) )
63		undif	\|- ( \|^\| ran U C_ ( t ` b ) <-> ( \|^\| ran U u. ( ( t ` b ) \ \|^\| ran U ) ) = ( t ` b ) )
64	62 63	sylib	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( \|^\| ran U u. ( ( t ` b ) \ \|^\| ran U ) ) = ( t ` b ) )
65	57 64	eqeq12d	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( \|^\| ran U u. ( ( t ` a ) \ \|^\| ran U ) ) = ( \|^\| ran U u. ( ( t ` b ) \ \|^\| ran U ) ) <-> ( t ` a ) = ( t ` b ) ) )
66	50 65	imbitrid	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( ( t ` a ) \ \|^\| ran U ) = ( ( t ` b ) \ \|^\| ran U ) -> ( t ` a ) = ( t ` b ) ) )
67	11	sseli	\|- ( a e. P -> a e. _om )
68	11	sseli	\|- ( b e. P -> b e. _om )
69	67 68	anim12i	\|- ( ( a e. P /\ b e. P ) -> ( a e. _om /\ b e. _om ) )
70		f1fveq	\|- ( ( t : _om -1-1-> _V /\ ( a e. _om /\ b e. _om ) ) -> ( ( t ` a ) = ( t ` b ) <-> a = b ) )
71	69 70	sylan2	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( t ` a ) = ( t ` b ) <-> a = b ) )
72	66 71	sylibd	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( ( t ` a ) \ \|^\| ran U ) = ( ( t ` b ) \ \|^\| ran U ) -> a = b ) )
73	49 72	sylbid	\|- ( ( t : _om -1-1-> _V /\ ( a e. P /\ b e. P ) ) -> ( ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` a ) = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` b ) -> a = b ) )
74	73	ralrimivva	\|- ( t : _om -1-1-> _V -> A. a e. P A. b e. P ( ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` a ) = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` b ) -> a = b ) )
75		dff13	\|- ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) : P -1-1-> _V <-> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) : P --> _V /\ A. a e. P A. b e. P ( ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` a ) = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) ` b ) -> a = b ) ) )
76	36 74 75	sylanbrc	\|- ( t : _om -1-1-> _V -> ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) : P -1-1-> _V )
77	4	fin23lem22	\|- ( ( P C_ _om /\ -. P e. Fin ) -> Q : _om -1-1-onto-> P )
78		f1of1	\|- ( Q : _om -1-1-onto-> P -> Q : _om -1-1-> P )
79	77 78	syl	\|- ( ( P C_ _om /\ -. P e. Fin ) -> Q : _om -1-1-> P )
80	11 79	mpan	\|- ( -. P e. Fin -> Q : _om -1-1-> P )
81		f1co	\|- ( ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) : P -1-1-> _V /\ Q : _om -1-1-> P ) -> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) : _om -1-1-> _V )
82	76 80 81	syl2an	\|- ( ( t : _om -1-1-> _V /\ -. P e. Fin ) -> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) : _om -1-1-> _V )
83		f1eq1	\|- ( Z = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) -> ( Z : _om -1-1-> _V <-> ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) : _om -1-1-> _V ) )
84	82 83	syl5ibrcom	\|- ( ( t : _om -1-1-> _V /\ -. P e. Fin ) -> ( Z = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) -> Z : _om -1-1-> _V ) )
85	84	impr	\|- ( ( t : _om -1-1-> _V /\ ( -. P e. Fin /\ Z = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) ) ) -> Z : _om -1-1-> _V )
86	29 85	jaodan	\|- ( ( t : _om -1-1-> _V /\ ( ( P e. Fin /\ Z = ( t o. R ) ) \/ ( -. P e. Fin /\ Z = ( ( z e. P \|-> ( ( t ` z ) \ \|^\| ran U ) ) o. Q ) ) ) ) -> Z : _om -1-1-> _V )
87	8 86	mpan2	\|- ( t : _om -1-1-> _V -> Z : _om -1-1-> _V )

Metamath Proof Explorer

Theorem fin23lem28

Proof