nrex1

Description: The class of signed reals is a set. Note that a shorter proof is possible using qsex (and not requiring enrer ), but it would add a dependency on ax-rep . (Contributed by Mario Carneiro, 17-Nov-2014) Extract proof from that of axcnex . (Revised by BJ, 4-Feb-2023) (New usage is discouraged.)

		Ref	Expression
	Assertion	nrex1	$⊢ 𝑹 \in V$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		npex	$⊢ 𝑷 \in V$
3	2 2	xpex	$⊢ 𝑷 \times 𝑷 \in V$
4	3	pwex	$⊢ 𝒫 (𝑷 \times 𝑷) \in V$
5		enrer	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$
6	5	a1i	$⊢ ⊤ \to ~_{𝑹} Er (𝑷 \times 𝑷)$
7	6	qsss	$⊢ ⊤ \to (𝑷 \times 𝑷) / ~_{𝑹} \subseteq 𝒫 (𝑷 \times 𝑷)$
8	7	mptru	$⊢ (𝑷 \times 𝑷) / ~_{𝑹} \subseteq 𝒫 (𝑷 \times 𝑷)$
9	4 8	ssexi	$⊢ (𝑷 \times 𝑷) / ~_{𝑹} \in V$
10	1 9	eqeltri	$⊢ 𝑹 \in V$

Metamath Proof Explorer

Theorem nrex1

Proof