Step |
Hyp |
Ref |
Expression |
1 |
|
ffvelrn |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) e. ( <_ i^i ( RR X. RR ) ) ) |
2 |
1
|
elin2d |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) e. ( RR X. RR ) ) |
3 |
|
1st2nd2 |
|- ( ( F ` N ) e. ( RR X. RR ) -> ( F ` N ) = <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. ) |
4 |
2 3
|
syl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( F ` N ) = <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. ) |
5 |
4 1
|
eqeltrrd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. ( <_ i^i ( RR X. RR ) ) ) |
6 |
|
ancom |
|- ( ( ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) /\ ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR ) ) <-> ( ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR ) /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) ) |
7 |
|
elin |
|- ( <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. ( <_ i^i ( RR X. RR ) ) <-> ( <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. <_ /\ <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. ( RR X. RR ) ) ) |
8 |
|
df-br |
|- ( ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) <-> <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. <_ ) |
9 |
8
|
bicomi |
|- ( <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. <_ <-> ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) |
10 |
|
opelxp |
|- ( <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. ( RR X. RR ) <-> ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR ) ) |
11 |
9 10
|
anbi12i |
|- ( ( <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. <_ /\ <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. ( RR X. RR ) ) <-> ( ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) /\ ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR ) ) ) |
12 |
7 11
|
bitri |
|- ( <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. ( <_ i^i ( RR X. RR ) ) <-> ( ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) /\ ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR ) ) ) |
13 |
|
df-3an |
|- ( ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) <-> ( ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR ) /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) ) |
14 |
6 12 13
|
3bitr4i |
|- ( <. ( 1st ` ( F ` N ) ) , ( 2nd ` ( F ` N ) ) >. e. ( <_ i^i ( RR X. RR ) ) <-> ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) ) |
15 |
5 14
|
sylib |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ N e. NN ) -> ( ( 1st ` ( F ` N ) ) e. RR /\ ( 2nd ` ( F ` N ) ) e. RR /\ ( 1st ` ( F ` N ) ) <_ ( 2nd ` ( F ` N ) ) ) ) |