Metamath Proof Explorer


Theorem ovolfcl

Description: Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolfcl
|- ( ( 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 ) ) ) )

Proof

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 ) ) ) )