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 ∈ 𝑃 )