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	⊢ Ⅎ 𝑘 𝜑
	hoissrrn2.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
	hoissrrn2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
Assertion	hoissrrn2	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		hoissrrn2.kph	⊢ Ⅎ 𝑘 𝜑
2		hoissrrn2.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
3		hoissrrn2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
4		ovex	⊢ ( 𝐴 [,) 𝐵 ) ∈ V
5	4	rgenw	⊢ ∀ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ∈ V
6		ixpssmapg	⊢ ( ∀ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ∈ V → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) )
7	5 6	ax-mp	⊢ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ↑m 𝑋 )
8	7	a1i	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) )
9		reex	⊢ ℝ ∈ V
10	9	a1i	⊢ ( 𝜑 → ℝ ∈ V )
11		icossre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
12	2 3 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
13	12	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 → ( 𝐴 [,) 𝐵 ) ⊆ ℝ ) )
14	1 13	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
15		iunss	⊢ ( ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ℝ ↔ ∀ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
16	14 15	sylibr	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
17		mapss	⊢ ( ( ℝ ∈ V ∧ ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ℝ ) → ( ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 ) )
18	10 16 17	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 ) )
19	8 18	sstrd	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) )