Theorem 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 )