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 |