Theorem hoissrrn

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

	Ref	Expression
Hypothesis	hoissrrn.1	|- ( ph -> I : X --> ( RR X. RR ) )
Assertion	hoissrrn	|- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) C_ ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		hoissrrn.1	|- ( ph -> I : X --> ( RR X. RR ) )
2		fvex	|- ( ( [,) o. I ) ` k ) e. _V
3	2	rgenw	|- A. k e. X ( ( [,) o. I ) ` k ) e. _V
4		ixpssmapg	|- ( A. k e. X ( ( [,) o. I ) ` k ) e. _V -> X_ k e. X ( ( [,) o. I ) ` k ) C_ ( U_ k e. X ( ( [,) o. I ) ` k ) ^m X ) )
5	3 4	ax-mp	|- X_ k e. X ( ( [,) o. I ) ` k ) C_ ( U_ k e. X ( ( [,) o. I ) ` k ) ^m X )
6	5	a1i	|- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) C_ ( U_ k e. X ( ( [,) o. I ) ` k ) ^m X ) )
7		reex	|- RR e. _V
8	7	a1i	|- ( ph -> RR e. _V )
9	1	hoissre	|- ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) C_ RR )
10	9	ralrimiva	|- ( ph -> A. k e. X ( ( [,) o. I ) ` k ) C_ RR )
11		iunss	|- ( U_ k e. X ( ( [,) o. I ) ` k ) C_ RR <-> A. k e. X ( ( [,) o. I ) ` k ) C_ RR )
12	10 11	sylibr	|- ( ph -> U_ k e. X ( ( [,) o. I ) ` k ) C_ RR )
13		mapss	|- ( ( RR e. _V /\ U_ k e. X ( ( [,) o. I ) ` k ) C_ RR ) -> ( U_ k e. X ( ( [,) o. I ) ` k ) ^m X ) C_ ( RR ^m X ) )
14	8 12 13	syl2anc	|- ( ph -> ( U_ k e. X ( ( [,) o. I ) ` k ) ^m X ) C_ ( RR ^m X ) )
15	6 14	sstrd	|- ( ph -> X_ k e. X ( ( [,) o. I ) ` k ) C_ ( RR ^m X ) )