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