Theorem 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\phi$$
	hoissrrn2.a	$$⊢\left(\phi \wedge k\in X\right)\to A\in ℝ$$
	hoissrrn2.b	$$⊢\left(\phi \wedge k\in X\right)\to B\in {ℝ}^{*}$$
Assertion	hoissrrn2	$$⊢\phi \to \underset{k\in X}{⨉}\left[A,B\right)\subseteq {ℝ}^X$$

Proof

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