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 ⊆ ℝ