Theorem ioosshoi

Description: A n-dimensional open interval is a subset of the half-open interval with the same bounds. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Assertion	ioosshoi	|- X_ k e. X ( A (,) B ) C_ X_ k e. X ( A [,) B )

Proof

Step	Hyp	Ref	Expression
1		nftru	|- F/ k T.
2		ioossico	|- ( A (,) B ) C_ ( A [,) B )
3	2	a1i	|- ( ( T. /\ k e. X ) -> ( A (,) B ) C_ ( A [,) B ) )
4	1 3	ixpssixp	|- ( T. -> X_ k e. X ( A (,) B ) C_ X_ k e. X ( A [,) B ) )
5	4	mptru	|- X_ k e. X ( A (,) B ) C_ X_ k e. X ( A [,) B )