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 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nftru	⊢ Ⅎ 𝑘 ⊤
2		ioossico	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,) 𝐵 )
3	2	a1i	⊢ ( ( ⊤ ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,) 𝐵 ) )
4	1 3	ixpssixp	⊢ ( ⊤ → X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) )
5	4	mptru	⊢ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 )