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	$$⊢\underset{k\in X}{⨉}\left(A,B\right)\subseteq \underset{k\in X}{⨉}\left[A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nftru	$$⊢Ⅎk\top$$
2		ioossico	$$⊢\left(A,B\right)\subseteq \left[A,B\right)$$
3	2	a1i	$$⊢\left(\top \wedge k\in X\right)\to \left(A,B\right)\subseteq \left[A,B\right)$$
4	1 3	ixpssixp	$$⊢\top \to \underset{k\in X}{⨉}\left(A,B\right)\subseteq \underset{k\in X}{⨉}\left[A,B\right)$$
5	4	mptru	$$⊢\underset{k\in X}{⨉}\left(A,B\right)\subseteq \underset{k\in X}{⨉}\left[A,B\right)$$