Theorem reexALT

Description: Alternate proof of reex . (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 23-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	reexALT	$$⊢ℝ\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		nnexALT	$$⊢\mathbb{N}\in \mathrm{V}$$
2		qexALT	$$⊢\mathbb{Q}\in \mathrm{V}$$
3	1 2	rpnnen1	$$⊢ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)$$
4		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
5	4	brrelex1i	$$⊢ℝ\preccurlyeq \left({\mathbb{Q}}^{\mathbb{N}}\right)\to ℝ\in \mathrm{V}$$
6	3 5	ax-mp	$$⊢ℝ\in \mathrm{V}$$