Theorem ringn0

Description: Rings exist. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Assertion	ringn0	$$⊢\mathrm{Ring}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢z\in \mathrm{V}$$
2		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}$$
3	2	ring1	$$⊢z\in \mathrm{V}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}\in \mathrm{Ring}$$
4		ne0i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{z\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨z,z⟩,z⟩\right\}⟩\right\}\in \mathrm{Ring}\to \mathrm{Ring}\ne \varnothing$$
5	1 3 4	mp2b	$$⊢\mathrm{Ring}\ne \varnothing$$