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	⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
Assertion	hoissrrn	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		hoissrrn.1	⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
2		fvex	⊢ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ V
3	2	rgenw	⊢ ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ V
4		ixpssmapg	⊢ ( ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ V → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) )
5	3 4	ax-mp	⊢ X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 )
6	5	a1i	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) )
7		reex	⊢ ℝ ∈ V
8	7	a1i	⊢ ( 𝜑 → ℝ ∈ V )
9	1	hoissre	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ )
10	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ )
11		iunss	⊢ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ↔ ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ )
12	10 11	sylibr	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ )
13		mapss	⊢ ( ( ℝ ∈ V ∧ ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ) → ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 ) )
14	8 12 13	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 ) )
15	6 14	sstrd	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) )