Metamath Proof Explorer


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