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	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
	rrx0el.p	$$⊢P={ℝ}^I$$
Assertion	rrx0el	$$⊢I\in V\to \underset{\dot{}}{0}\in P$$

Proof

Step	Hyp	Ref	Expression
1		rrx0el.0	$$⊢\underset{\dot{}}{0}=I\times \left\{0\right\}$$
2		rrx0el.p	$$⊢P={ℝ}^I$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4	3	fconst	$$⊢\left(I\times \left\{0\right\}\right):I⟶\left\{0\right\}$$
5	4	a1i	$$⊢I\in V\to \left(I\times \left\{0\right\}\right):I⟶\left\{0\right\}$$
6		0re	$$⊢0\in ℝ$$
7		snssg	$$⊢0\in ℝ\to \left(0\in ℝ\leftrightarrow \left\{0\right\}\subseteq ℝ\right)$$
8	6 7	ax-mp	$$⊢0\in ℝ\leftrightarrow \left\{0\right\}\subseteq ℝ$$
9	6 8	mpbi	$$⊢\left\{0\right\}\subseteq ℝ$$
10	9	a1i	$$⊢I\in V\to \left\{0\right\}\subseteq ℝ$$
11	5 10	fssd	$$⊢I\in V\to \left(I\times \left\{0\right\}\right):I⟶ℝ$$
12		reex	$$⊢ℝ\in \mathrm{V}$$
13	12	a1i	$$⊢I\in V\to ℝ\in \mathrm{V}$$
14		id	$$⊢I\in V\to I\in V$$
15	13 14	elmapd	$$⊢I\in V\to \left(I\times \left\{0\right\}\in \left({ℝ}^I\right)\leftrightarrow \left(I\times \left\{0\right\}\right):I⟶ℝ\right)$$
16	11 15	mpbird	$$⊢I\in V\to I\times \left\{0\right\}\in \left({ℝ}^I\right)$$
17	16 1 2	3eltr4g	$$⊢I\in V\to \underset{\dot{}}{0}\in P$$