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 φ I : X 2
hoicoto2.a A = k X 1 st I k
hoicoto2.b B = k X 2 nd I k
Assertion hoicoto2 φ k X . I k = k X A k B k

Proof

Step Hyp Ref Expression
1 hoicoto2.i φ I : X 2
2 hoicoto2.a A = k X 1 st I k
3 hoicoto2.b B = k X 2 nd I k
4 1 adantr φ k X I : X 2
5 simpr φ k X k X
6 4 5 fvovco φ k X . I k = 1 st I k 2 nd I k
7 1 ffvelrnda φ k X I k 2
8 xp1st I k 2 1 st I k
9 7 8 syl φ k X 1 st I k
10 9 elexd φ k X 1 st I k V
11 2 fvmpt2 k X 1 st I k V A k = 1 st I k
12 5 10 11 syl2anc φ k X A k = 1 st I k
13 12 eqcomd φ k X 1 st I k = A k
14 xp2nd I k 2 2 nd I k
15 7 14 syl φ k X 2 nd I k
16 15 elexd φ k X 2 nd I k V
17 3 fvmpt2 k X 2 nd I k V B k = 2 nd I k
18 5 16 17 syl2anc φ k X B k = 2 nd I k
19 18 eqcomd φ k X 2 nd I k = B k
20 13 19 oveq12d φ k X 1 st I k 2 nd I k = A k B k
21 6 20 eqtrd φ k X . I k = A k B k
22 21 ixpeq2dva φ k X . I k = k X A k B k