hoissrrn

Description: A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Hypothesis	hoissrrn.1	$⊢ φ \to I : X ⟶ ℝ^{2}$
	Assertion	hoissrrn	$⊢ φ \to \underset{k \in X}{⨉} ([.) \circ I) (k) \subseteq ℝ^{X}$

Step	Hyp	Ref	Expression
1		hoissrrn.1	$⊢ φ \to I : X ⟶ ℝ^{2}$
2		fvex	$⊢ ([.) \circ I) (k) \in V$
3	2	rgenw	$⊢ \forall k \in X ([.) \circ I) (k) \in V$
4		ixpssmapg	$⊢ \forall k \in X ([.) \circ I) (k) \in V \to \underset{k \in X}{⨉} ([.) \circ I) (k) \subseteq {⋃_{k \in X} ([.) \circ I) (k)}^{X}$
5	3 4	ax-mp	$⊢ \underset{k \in X}{⨉} ([.) \circ I) (k) \subseteq {⋃_{k \in X} ([.) \circ I) (k)}^{X}$
6	5	a1i	$⊢ φ \to \underset{k \in X}{⨉} ([.) \circ I) (k) \subseteq {⋃_{k \in X} ([.) \circ I) (k)}^{X}$
7		reex	$⊢ ℝ \in V$
8	7	a1i	$⊢ φ \to ℝ \in V$
9	1	hoissre	$⊢ (φ \land k \in X) \to ([.) \circ I) (k) \subseteq ℝ$
10	9	ralrimiva	$⊢ φ \to \forall k \in X ([.) \circ I) (k) \subseteq ℝ$
11		iunss	$⊢ ⋃_{k \in X} ([.) \circ I) (k) \subseteq ℝ \leftrightarrow \forall k \in X ([.) \circ I) (k) \subseteq ℝ$
12	10 11	sylibr	$⊢ φ \to ⋃_{k \in X} ([.) \circ I) (k) \subseteq ℝ$
13		mapss	$⊢ (ℝ \in V \land ⋃_{k \in X} ([.) \circ I) (k) \subseteq ℝ) \to {⋃_{k \in X} ([.) \circ I) (k)}^{X} \subseteq ℝ^{X}$
14	8 12 13	syl2anc	$⊢ φ \to {⋃_{k \in X} ([.) \circ I) (k)}^{X} \subseteq ℝ^{X}$
15	6 14	sstrd	$⊢ φ \to \underset{k \in X}{⨉} ([.) \circ I) (k) \subseteq ℝ^{X}$

Metamath Proof Explorer