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	$⊢ φ \to I : X ⟶ ℝ^{2}$
	Assertion	hoissre	$⊢ (φ \land k \in X) \to ([.) \circ I) (k) \subseteq ℝ$

Step	Hyp	Ref	Expression
1		hoissre.1	$⊢ φ \to I : X ⟶ ℝ^{2}$
2	1	adantr	$⊢ (φ \land k \in X) \to I : X ⟶ ℝ^{2}$
3		simpr	$⊢ (φ \land k \in X) \to k \in X$
4	2 3	fvovco	$⊢ (φ \land k \in X) \to ([.) \circ I) (k) = [1^{st} (I (k)), 2^{nd} (I (k)))$
5	1	ffvelcdmda	$⊢ (φ \land k \in X) \to I (k) \in ℝ^{2}$
6		xp1st	$⊢ I (k) \in ℝ^{2} \to 1^{st} (I (k)) \in ℝ$
7	5 6	syl	$⊢ (φ \land k \in X) \to 1^{st} (I (k)) \in ℝ$
8		xp2nd	$⊢ I (k) \in ℝ^{2} \to 2^{nd} (I (k)) \in ℝ$
9	5 8	syl	$⊢ (φ \land k \in X) \to 2^{nd} (I (k)) \in ℝ$
10	9	rexrd	$⊢ (φ \land k \in X) \to 2^{nd} (I (k)) \in ℝ^{*}$
11		icossre	$⊢ (1^{st} (I (k)) \in ℝ \land 2^{nd} (I (k)) \in ℝ^{*}) \to [1^{st} (I (k)), 2^{nd} (I (k))) \subseteq ℝ$
12	7 10 11	syl2anc	$⊢ (φ \land k \in X) \to [1^{st} (I (k)), 2^{nd} (I (k))) \subseteq ℝ$
13	4 12	eqsstrd	$⊢ (φ \land k \in X) \to ([.) \circ I) (k) \subseteq ℝ$

Metamath Proof Explorer