Metamath Proof Explorer

Theorem hoi2toco

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 hoi2toco.1 
|- F/ k ph
hoi2toco.c 
|- I = ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. )
Assertion hoi2toco 
|- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )

Proof

Step Hyp Ref Expression
1 hoi2toco.1 
 |-  F/ k ph
2 hoi2toco.c 
 |-  I = ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. )
3 2 funmpt2 
 |-  Fun I
4 3 a1i 
 |-  ( ph -> Fun I )
5 4 adantr 
 |-  ( ( ph /\ k e. X ) -> Fun I )
6 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
7 2 dmeqi 
 |-  dom I = dom ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. )
8 7 a1i 
 |-  ( ph -> dom I = dom ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) )
9 opex 
 |-  <. ( A ` k ) , ( B ` k ) >. e. _V
10 9 2a1i 
 |-  ( ph -> ( k e. X -> <. ( A ` k ) , ( B ` k ) >. e. _V ) )
11 1 10 ralrimi 
 |-  ( ph -> A. k e. X <. ( A ` k ) , ( B ` k ) >. e. _V )
12 dmmptg 
 |-  ( A. k e. X <. ( A ` k ) , ( B ` k ) >. e. _V -> dom ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) = X )
13 11 12 syl 
 |-  ( ph -> dom ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) = X )
14 8 13 eqtr2d 
 |-  ( ph -> X = dom I )
15 14 adantr 
 |-  ( ( ph /\ k e. X ) -> X = dom I )
16 6 15 eleqtrd 
 |-  ( ( ph /\ k e. X ) -> k e. dom I )
17 fvco 
 |-  ( ( Fun I /\ k e. dom I ) -> ( ( [,) o. I ) ` k ) = ( [,) ` ( I ` k ) ) )
18 5 16 17 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) = ( [,) ` ( I ` k ) ) )
19 9 a1i 
 |-  ( ( ph /\ k e. X ) -> <. ( A ` k ) , ( B ` k ) >. e. _V )
20 2 fvmpt2 
 |-  ( ( k e. X /\ <. ( A ` k ) , ( B ` k ) >. e. _V ) -> ( I ` k ) = <. ( A ` k ) , ( B ` k ) >. )
21 6 19 20 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( I ` k ) = <. ( A ` k ) , ( B ` k ) >. )
22 21 fveq2d 
 |-  ( ( ph /\ k e. X ) -> ( [,) ` ( I ` k ) ) = ( [,) ` <. ( A ` k ) , ( B ` k ) >. ) )
23 df-ov 
 |-  ( ( A ` k ) [,) ( B ` k ) ) = ( [,) ` <. ( A ` k ) , ( B ` k ) >. )
24 23 eqcomi 
 |-  ( [,) ` <. ( A ` k ) , ( B ` k ) >. ) = ( ( A ` k ) [,) ( B ` k ) )
25 24 a1i 
 |-  ( ( ph /\ k e. X ) -> ( [,) ` <. ( A ` k ) , ( B ` k ) >. ) = ( ( A ` k ) [,) ( B ` k ) ) )
26 18 22 25 3eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) = ( ( A ` k ) [,) ( B ` k ) ) )
27 1 26 ixpeq2d 
 |-  ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )