Metamath Proof Explorer

Theorem hoissre

Description: The projection of a half-open interval onto a single dimension is a subset of RR . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis hoissre.1 
|- ( ph -> I : X --> ( RR X. RR ) )
Assertion hoissre 
|- ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) C_ RR )

Proof

Step Hyp Ref Expression
1 hoissre.1 
 |-  ( ph -> I : X --> ( RR X. RR ) )
2 1 adantr 
 |-  ( ( ph /\ k e. X ) -> I : X --> ( RR X. RR ) )
3 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
4 2 3 fvovco 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) = ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) )
5 1 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( I ` k ) e. ( RR X. RR ) )
6 xp1st 
 |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 1st ` ( I ` k ) ) e. RR )
7 5 6 syl 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( I ` k ) ) e. RR )
8 xp2nd 
 |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 2nd ` ( I ` k ) ) e. RR )
9 5 8 syl 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. RR )
10 9 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. RR* )
11 icossre 
 |-  ( ( ( 1st ` ( I ` k ) ) e. RR /\ ( 2nd ` ( I ` k ) ) e. RR* ) -> ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) C_ RR )
12 7 10 11 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) C_ RR )
13 4 12 eqsstrd 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) C_ RR )