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	|- F/ k ph
	hoissrrn2.a	|- ( ( ph /\ k e. X ) -> A e. RR )
	hoissrrn2.b	|- ( ( ph /\ k e. X ) -> B e. RR* )
Assertion	hoissrrn2	|- ( ph -> X_ k e. X ( A [,) B ) C_ ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		hoissrrn2.kph	|- F/ k ph
2		hoissrrn2.a	|- ( ( ph /\ k e. X ) -> A e. RR )
3		hoissrrn2.b	|- ( ( ph /\ k e. X ) -> B e. RR* )
4		ovex	|- ( A [,) B ) e. _V
5	4	rgenw	|- A. k e. X ( A [,) B ) e. _V
6		ixpssmapg	|- ( A. k e. X ( A [,) B ) e. _V -> X_ k e. X ( A [,) B ) C_ ( U_ k e. X ( A [,) B ) ^m X ) )
7	5 6	ax-mp	|- X_ k e. X ( A [,) B ) C_ ( U_ k e. X ( A [,) B ) ^m X )
8	7	a1i	|- ( ph -> X_ k e. X ( A [,) B ) C_ ( U_ k e. X ( A [,) B ) ^m X ) )
9		reex	|- RR e. _V
10	9	a1i	|- ( ph -> RR e. _V )
11		icossre	|- ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) C_ RR )
12	2 3 11	syl2anc	|- ( ( ph /\ k e. X ) -> ( A [,) B ) C_ RR )
13	12	ex	|- ( ph -> ( k e. X -> ( A [,) B ) C_ RR ) )
14	1 13	ralrimi	|- ( ph -> A. k e. X ( A [,) B ) C_ RR )
15		iunss	|- ( U_ k e. X ( A [,) B ) C_ RR <-> A. k e. X ( A [,) B ) C_ RR )
16	14 15	sylibr	|- ( ph -> U_ k e. X ( A [,) B ) C_ RR )
17		mapss	|- ( ( RR e. _V /\ U_ k e. X ( A [,) B ) C_ RR ) -> ( U_ k e. X ( A [,) B ) ^m X ) C_ ( RR ^m X ) )
18	10 16 17	syl2anc	|- ( ph -> ( U_ k e. X ( A [,) B ) ^m X ) C_ ( RR ^m X ) )
19	8 18	sstrd	|- ( ph -> X_ k e. X ( A [,) B ) C_ ( RR ^m X ) )