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 φ I : X 2
Assertion hoissre φ k X . I k

Proof

Step Hyp Ref Expression
1 hoissre.1 φ I : X 2
2 1 adantr φ k X I : X 2
3 simpr φ k X k X
4 2 3 fvovco φ k X . I k = 1 st I k 2 nd I k
5 1 ffvelrnda φ k X I k 2
6 xp1st I k 2 1 st I k
7 5 6 syl φ k X 1 st I k
8 xp2nd I k 2 2 nd I k
9 5 8 syl φ k X 2 nd I k
10 9 rexrd φ k X 2 nd I k *
11 icossre 1 st I k 2 nd I k * 1 st I k 2 nd I k
12 7 10 11 syl2anc φ k X 1 st I k 2 nd I k
13 4 12 eqsstrd φ k X . I k