hoissrrn2

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

	Ref	Expression
Hypotheses	hoissrrn2.kph	$⊢ Ⅎ k φ$
	hoissrrn2.a	$⊢ (φ \land k \in X) \to A \in ℝ$
	hoissrrn2.b	$⊢ (φ \land k \in X) \to B \in ℝ^{*}$
Assertion	hoissrrn2	$⊢ φ \to \underset{k \in X}{⨉} [A, B) \subseteq ℝ^{X}$

Step	Hyp	Ref	Expression
1		hoissrrn2.kph	$⊢ Ⅎ k φ$
2		hoissrrn2.a	$⊢ (φ \land k \in X) \to A \in ℝ$
3		hoissrrn2.b	$⊢ (φ \land k \in X) \to B \in ℝ^{*}$
4		ovex	$⊢ [A, B) \in V$
5	4	rgenw	$⊢ \forall k \in X [A, B) \in V$
6		ixpssmapg	$⊢ \forall k \in X [A, B) \in V \to \underset{k \in X}{⨉} [A, B) \subseteq {⋃_{k \in X} [A, B)}^{X}$
7	5 6	ax-mp	$⊢ \underset{k \in X}{⨉} [A, B) \subseteq {⋃_{k \in X} [A, B)}^{X}$
8	7	a1i	$⊢ φ \to \underset{k \in X}{⨉} [A, B) \subseteq {⋃_{k \in X} [A, B)}^{X}$
9		reex	$⊢ ℝ \in V$
10	9	a1i	$⊢ φ \to ℝ \in V$
11		icossre	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \subseteq ℝ$
12	2 3 11	syl2anc	$⊢ (φ \land k \in X) \to [A, B) \subseteq ℝ$
13	12	ex	$⊢ φ \to (k \in X \to [A, B) \subseteq ℝ)$
14	1 13	ralrimi	$⊢ φ \to \forall k \in X [A, B) \subseteq ℝ$
15		iunss	$⊢ ⋃_{k \in X} [A, B) \subseteq ℝ \leftrightarrow \forall k \in X [A, B) \subseteq ℝ$
16	14 15	sylibr	$⊢ φ \to ⋃_{k \in X} [A, B) \subseteq ℝ$
17		mapss	$⊢ (ℝ \in V \land ⋃_{k \in X} [A, B) \subseteq ℝ) \to {⋃_{k \in X} [A, B)}^{X} \subseteq ℝ^{X}$
18	10 16 17	syl2anc	$⊢ φ \to {⋃_{k \in X} [A, B)}^{X} \subseteq ℝ^{X}$
19	8 18	sstrd	$⊢ φ \to \underset{k \in X}{⨉} [A, B) \subseteq ℝ^{X}$

Metamath Proof Explorer