Metamath Proof Explorer


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 𝑋 ) )