Metamath Proof Explorer

Theorem hoicoto2

Description: The half-open interval expressed using a composition of a function into ( RR X. RR ) and using two distinct real-valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoicoto2.i 
|- ( ph -> I : X --> ( RR X. RR ) )
hoicoto2.a 
|- A = ( k e. X |-> ( 1st ` ( I ` k ) ) )
hoicoto2.b 
|- B = ( k e. X |-> ( 2nd ` ( I ` k ) ) )
Assertion hoicoto2 
|- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )

Proof

Step Hyp Ref Expression
1 hoicoto2.i 
 |-  ( ph -> I : X --> ( RR X. RR ) )
2 hoicoto2.a 
 |-  A = ( k e. X |-> ( 1st ` ( I ` k ) ) )
3 hoicoto2.b 
 |-  B = ( k e. X |-> ( 2nd ` ( I ` k ) ) )
4 1 adantr 
 |-  ( ( ph /\ k e. X ) -> I : X --> ( RR X. RR ) )
5 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
6 4 5 fvovco 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) = ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) )
7 1 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( I ` k ) e. ( RR X. RR ) )
8 xp1st 
 |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 1st ` ( I ` k ) ) e. RR )
9 7 8 syl 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( I ` k ) ) e. RR )
10 9 elexd 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( I ` k ) ) e. _V )
11 2 fvmpt2 
 |-  ( ( k e. X /\ ( 1st ` ( I ` k ) ) e. _V ) -> ( A ` k ) = ( 1st ` ( I ` k ) ) )
12 5 10 11 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) = ( 1st ` ( I ` k ) ) )
13 12 eqcomd 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( I ` k ) ) = ( A ` k ) )
14 xp2nd 
 |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 2nd ` ( I ` k ) ) e. RR )
15 7 14 syl 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. RR )
16 15 elexd 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. _V )
17 3 fvmpt2 
 |-  ( ( k e. X /\ ( 2nd ` ( I ` k ) ) e. _V ) -> ( B ` k ) = ( 2nd ` ( I ` k ) ) )
18 5 16 17 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) = ( 2nd ` ( I ` k ) ) )
19 18 eqcomd 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) = ( B ` k ) )
20 13 19 oveq12d 
 |-  ( ( ph /\ k e. X ) -> ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
21 6 20 eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) = ( ( A ` k ) [,) ( B ` k ) ) )
22 21 ixpeq2dva 
 |-  ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )