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 kφ
hoi2toco.c I=kXAkBk
Assertion hoi2toco φkX.Ik=kXAkBk

Proof

Step Hyp Ref Expression
1 hoi2toco.1 kφ
2 hoi2toco.c I=kXAkBk
3 2 funmpt2 FunI
4 3 a1i φFunI
5 4 adantr φkXFunI
6 simpr φkXkX
7 2 dmeqi domI=domkXAkBk
8 7 a1i φdomI=domkXAkBk
9 opex AkBkV
10 9 2a1i φkXAkBkV
11 1 10 ralrimi φkXAkBkV
12 dmmptg kXAkBkVdomkXAkBk=X
13 11 12 syl φdomkXAkBk=X
14 8 13 eqtr2d φX=domI
15 14 adantr φkXX=domI
16 6 15 eleqtrd φkXkdomI
17 fvco FunIkdomI.Ik=.Ik
18 5 16 17 syl2anc φkX.Ik=.Ik
19 9 a1i φkXAkBkV
20 2 fvmpt2 kXAkBkVIk=AkBk
21 6 19 20 syl2anc φkXIk=AkBk
22 21 fveq2d φkX.Ik=.AkBk
23 df-ov AkBk=.AkBk
24 23 eqcomi .AkBk=AkBk
25 24 a1i φkX.AkBk=AkBk
26 18 22 25 3eqtrd φkX.Ik=AkBk
27 1 26 ixpeq2d φkX.Ik=kXAkBk