Theorem rpex

Description: The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	rpex	$$⊢{ℝ}^{+}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
2	1	rpmsubg	$$⊢{ℝ}^{+}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
3	2	elexi	$$⊢{ℝ}^{+}\in \mathrm{V}$$