Theorem seqomlem2

Description: Lemma for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 23-Jun-2015)

	Ref	Expression
Hypothesis	seqomlem.a	|- Q = rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
Assertion	seqomlem2	|- ( Q " _om ) Fn _om

Proof

Step	Hyp	Ref	Expression
1		seqomlem.a	|- Q = rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
2		frfnom	|- ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) Fn _om
3	1	reseq1i	|- ( Q |` _om ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om )
4	3	fneq1i	|- ( ( Q |` _om ) Fn _om <-> ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) Fn _om )
5	2 4	mpbir	|- ( Q |` _om ) Fn _om
6		fvres	|- ( b e. _om -> ( ( Q |` _om ) ` b ) = ( Q ` b ) )
7	1	seqomlem1	|- ( b e. _om -> ( Q ` b ) = <. b , ( 2nd ` ( Q ` b ) ) >. )
8	6 7	eqtrd	|- ( b e. _om -> ( ( Q |` _om ) ` b ) = <. b , ( 2nd ` ( Q ` b ) ) >. )
9		fvex	|- ( 2nd ` ( Q ` b ) ) e. _V
10		opelxpi	|- ( ( b e. _om /\ ( 2nd ` ( Q ` b ) ) e. _V ) -> <. b , ( 2nd ` ( Q ` b ) ) >. e. ( _om X. _V ) )
11	9 10	mpan2	|- ( b e. _om -> <. b , ( 2nd ` ( Q ` b ) ) >. e. ( _om X. _V ) )
12	8 11	eqeltrd	|- ( b e. _om -> ( ( Q |` _om ) ` b ) e. ( _om X. _V ) )
13	12	rgen	|- A. b e. _om ( ( Q |` _om ) ` b ) e. ( _om X. _V )
14		ffnfv	|- ( ( Q |` _om ) : _om --> ( _om X. _V ) <-> ( ( Q |` _om ) Fn _om /\ A. b e. _om ( ( Q |` _om ) ` b ) e. ( _om X. _V ) ) )
15	5 13 14	mpbir2an	|- ( Q |` _om ) : _om --> ( _om X. _V )
16		frn	|- ( ( Q |` _om ) : _om --> ( _om X. _V ) -> ran ( Q |` _om ) C_ ( _om X. _V ) )
17	15 16	ax-mp	|- ran ( Q |` _om ) C_ ( _om X. _V )
18		df-br	|- ( a ran ( Q |` _om ) b <-> <. a , b >. e. ran ( Q |` _om ) )
19		fvelrnb	|- ( ( Q |` _om ) Fn _om -> ( <. a , b >. e. ran ( Q |` _om ) <-> E. c e. _om ( ( Q |` _om ) ` c ) = <. a , b >. ) )
20	5 19	ax-mp	|- ( <. a , b >. e. ran ( Q |` _om ) <-> E. c e. _om ( ( Q |` _om ) ` c ) = <. a , b >. )
21		fvres	|- ( c e. _om -> ( ( Q |` _om ) ` c ) = ( Q ` c ) )
22	21	eqeq1d	|- ( c e. _om -> ( ( ( Q |` _om ) ` c ) = <. a , b >. <-> ( Q ` c ) = <. a , b >. ) )
23	22	rexbiia	|- ( E. c e. _om ( ( Q |` _om ) ` c ) = <. a , b >. <-> E. c e. _om ( Q ` c ) = <. a , b >. )
24	18 20 23	3bitri	|- ( a ran ( Q |` _om ) b <-> E. c e. _om ( Q ` c ) = <. a , b >. )
25	1	seqomlem1	|- ( c e. _om -> ( Q ` c ) = <. c , ( 2nd ` ( Q ` c ) ) >. )
26	25	adantl	|- ( ( a e. _om /\ c e. _om ) -> ( Q ` c ) = <. c , ( 2nd ` ( Q ` c ) ) >. )
27	26	eqeq1d	|- ( ( a e. _om /\ c e. _om ) -> ( ( Q ` c ) = <. a , b >. <-> <. c , ( 2nd ` ( Q ` c ) ) >. = <. a , b >. ) )
28		vex	|- c e. _V
29		fvex	|- ( 2nd ` ( Q ` c ) ) e. _V
30	28 29	opth1	|- ( <. c , ( 2nd ` ( Q ` c ) ) >. = <. a , b >. -> c = a )
31	27 30	syl6bi	|- ( ( a e. _om /\ c e. _om ) -> ( ( Q ` c ) = <. a , b >. -> c = a ) )
32		fveqeq2	|- ( c = a -> ( ( Q ` c ) = <. a , b >. <-> ( Q ` a ) = <. a , b >. ) )
33	32	biimpd	|- ( c = a -> ( ( Q ` c ) = <. a , b >. -> ( Q ` a ) = <. a , b >. ) )
34	31 33	syli	|- ( ( a e. _om /\ c e. _om ) -> ( ( Q ` c ) = <. a , b >. -> ( Q ` a ) = <. a , b >. ) )
35		fveq2	|- ( ( Q ` a ) = <. a , b >. -> ( 2nd ` ( Q ` a ) ) = ( 2nd ` <. a , b >. ) )
36		vex	|- a e. _V
37		vex	|- b e. _V
38	36 37	op2nd	|- ( 2nd ` <. a , b >. ) = b
39	35 38	eqtr2di	|- ( ( Q ` a ) = <. a , b >. -> b = ( 2nd ` ( Q ` a ) ) )
40	34 39	syl6	|- ( ( a e. _om /\ c e. _om ) -> ( ( Q ` c ) = <. a , b >. -> b = ( 2nd ` ( Q ` a ) ) ) )
41	40	rexlimdva	|- ( a e. _om -> ( E. c e. _om ( Q ` c ) = <. a , b >. -> b = ( 2nd ` ( Q ` a ) ) ) )
42	1	seqomlem1	|- ( a e. _om -> ( Q ` a ) = <. a , ( 2nd ` ( Q ` a ) ) >. )
43		fveqeq2	|- ( c = a -> ( ( Q ` c ) = <. a , ( 2nd ` ( Q ` a ) ) >. <-> ( Q ` a ) = <. a , ( 2nd ` ( Q ` a ) ) >. ) )
44	43	rspcev	|- ( ( a e. _om /\ ( Q ` a ) = <. a , ( 2nd ` ( Q ` a ) ) >. ) -> E. c e. _om ( Q ` c ) = <. a , ( 2nd ` ( Q ` a ) ) >. )
45	42 44	mpdan	|- ( a e. _om -> E. c e. _om ( Q ` c ) = <. a , ( 2nd ` ( Q ` a ) ) >. )
46		opeq2	|- ( b = ( 2nd ` ( Q ` a ) ) -> <. a , b >. = <. a , ( 2nd ` ( Q ` a ) ) >. )
47	46	eqeq2d	|- ( b = ( 2nd ` ( Q ` a ) ) -> ( ( Q ` c ) = <. a , b >. <-> ( Q ` c ) = <. a , ( 2nd ` ( Q ` a ) ) >. ) )
48	47	rexbidv	|- ( b = ( 2nd ` ( Q ` a ) ) -> ( E. c e. _om ( Q ` c ) = <. a , b >. <-> E. c e. _om ( Q ` c ) = <. a , ( 2nd ` ( Q ` a ) ) >. ) )
49	45 48	syl5ibrcom	|- ( a e. _om -> ( b = ( 2nd ` ( Q ` a ) ) -> E. c e. _om ( Q ` c ) = <. a , b >. ) )
50	41 49	impbid	|- ( a e. _om -> ( E. c e. _om ( Q ` c ) = <. a , b >. <-> b = ( 2nd ` ( Q ` a ) ) ) )
51	24 50	syl5bb	|- ( a e. _om -> ( a ran ( Q |` _om ) b <-> b = ( 2nd ` ( Q ` a ) ) ) )
52	51	alrimiv	|- ( a e. _om -> A. b ( a ran ( Q |` _om ) b <-> b = ( 2nd ` ( Q ` a ) ) ) )
53		fvex	|- ( 2nd ` ( Q ` a ) ) e. _V
54		eqeq2	|- ( c = ( 2nd ` ( Q ` a ) ) -> ( b = c <-> b = ( 2nd ` ( Q ` a ) ) ) )
55	54	bibi2d	|- ( c = ( 2nd ` ( Q ` a ) ) -> ( ( a ran ( Q |` _om ) b <-> b = c ) <-> ( a ran ( Q |` _om ) b <-> b = ( 2nd ` ( Q ` a ) ) ) ) )
56	55	albidv	|- ( c = ( 2nd ` ( Q ` a ) ) -> ( A. b ( a ran ( Q |` _om ) b <-> b = c ) <-> A. b ( a ran ( Q |` _om ) b <-> b = ( 2nd ` ( Q ` a ) ) ) ) )
57	53 56	spcev	|- ( A. b ( a ran ( Q |` _om ) b <-> b = ( 2nd ` ( Q ` a ) ) ) -> E. c A. b ( a ran ( Q |` _om ) b <-> b = c ) )
58	52 57	syl	|- ( a e. _om -> E. c A. b ( a ran ( Q |` _om ) b <-> b = c ) )
59		eu6	|- ( E! b a ran ( Q |` _om ) b <-> E. c A. b ( a ran ( Q |` _om ) b <-> b = c ) )
60	58 59	sylibr	|- ( a e. _om -> E! b a ran ( Q |` _om ) b )
61	60	rgen	|- A. a e. _om E! b a ran ( Q |` _om ) b
62		dff3	|- ( ran ( Q |` _om ) : _om --> _V <-> ( ran ( Q |` _om ) C_ ( _om X. _V ) /\ A. a e. _om E! b a ran ( Q |` _om ) b ) )
63	17 61 62	mpbir2an	|- ran ( Q |` _om ) : _om --> _V
64		df-ima	|- ( Q " _om ) = ran ( Q |` _om )
65	64	feq1i	|- ( ( Q " _om ) : _om --> _V <-> ran ( Q |` _om ) : _om --> _V )
66	63 65	mpbir	|- ( Q " _om ) : _om --> _V
67		dffn2	|- ( ( Q " _om ) Fn _om <-> ( Q " _om ) : _om --> _V )
68	66 67	mpbir	|- ( Q " _om ) Fn _om