This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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	⊢ R ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-nr	⊢ R = ( ( P × P ) / ~_R )
2		npex	⊢ P ∈ V
3	2 2	xpex	⊢ ( P × P ) ∈ V
4	3	pwex	⊢ 𝒫 ( P × P ) ∈ V
5		enrer	⊢ ~_R Er ( P × P )
6	5	a1i	⊢ ( ⊤ → ~_R Er ( P × P ) )
7	6	qsss	⊢ ( ⊤ → ( ( P × P ) / ~_R ) ⊆ 𝒫 ( P × P ) )
8	7	mptru	⊢ ( ( P × P ) / ~_R ) ⊆ 𝒫 ( P × P )
9	4 8	ssexi	⊢ ( ( P × P ) / ~_R ) ∈ V
10	1 9	eqeltri	⊢ R ∈ V