This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrx0el

Description: The zero ("origin") in a generalized real Euclidean space is an element of its base set. (Contributed by AV, 11-Feb-2023)

Ref Expression
Hypotheses rrx0el.0 ⊢ 0 = ( 𝐼 × { 0 } )
rrx0el.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion rrx0el ( 𝐼 ∈ 𝑉 → 0 ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 rrx0el.0 ⊢ 0 = ( 𝐼 × { 0 } )
2 rrx0el.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3 c0ex ⊢ 0 ∈ V
4 3 fconst ⊢ ( 𝐼 × { 0 } ) : 𝐼 ⟶ { 0 }
5 4 a1i ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) : 𝐼 ⟶ { 0 } )
6 0re ⊢ 0 ∈ ℝ
7 snssg ⊢ ( 0 ∈ ℝ → ( 0 ∈ ℝ ↔ { 0 } ⊆ ℝ ) )
8 6 7 ax-mp ⊢ ( 0 ∈ ℝ ↔ { 0 } ⊆ ℝ )
9 6 8 mpbi ⊢ { 0 } ⊆ ℝ
10 9 a1i ⊢ ( 𝐼 ∈ 𝑉 → { 0 } ⊆ ℝ )
11 5 10 fssd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℝ )
12 reex ⊢ ℝ ∈ V
13 12 a1i ⊢ ( 𝐼 ∈ 𝑉 → ℝ ∈ V )
14 id ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉 )
15 13 14 elmapd ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝐼 × { 0 } ) ∈ ( ℝ ↑m 𝐼 ) ↔ ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℝ ) )
16 11 15 mpbird ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) ∈ ( ℝ ↑m 𝐼 ) )
17 16 1 2 3eltr4g ⊢ ( 𝐼 ∈ 𝑉 → 0 ∈ 𝑃 )