This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi 
 |-  ( ( 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 bitrid 
 |-  ( 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