df-enr

Description: Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.1 of Gleason p. 126. (Contributed by NM, 25-Jul-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-enr	$⊢ ~_{𝑹} = \{⟨x, y⟩ \| ((x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cer	$class ~_{𝑹}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cnp	$class 𝑷$
5	4 4	cxp	$class (𝑷 \times 𝑷)$
6	3 5	wcel	$wff x \in (𝑷 \times 𝑷)$
7	2	cv	$setvar y$
8	7 5	wcel	$wff y \in (𝑷 \times 𝑷)$
9	6 8	wa	$wff (x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷))$
10		vz	$setvar z$
11		vw	$setvar w$
12		vv	$setvar v$
13		vu	$setvar u$
14	10	cv	$setvar z$
15	11	cv	$setvar w$
16	14 15	cop	$class ⟨z, w⟩$
17	3 16	wceq	$wff x = ⟨z, w⟩$
18	12	cv	$setvar v$
19	13	cv	$setvar u$
20	18 19	cop	$class ⟨v, u⟩$
21	7 20	wceq	$wff y = ⟨v, u⟩$
22	17 21	wa	$wff (x = ⟨z, w⟩ \land y = ⟨v, u⟩)$
23		cpp	$class +_{𝑷}$
24	14 19 23	co	$class (z +_{𝑷} u)$
25	15 18 23	co	$class (w +_{𝑷} v)$
26	24 25	wceq	$wff z +_{𝑷} u = w +_{𝑷} v$
27	22 26	wa	$wff ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v)$
28	27 13	wex	$wff \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v)$
29	28 12	wex	$wff \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v)$
30	29 11	wex	$wff \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v)$
31	30 10	wex	$wff \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v)$
32	9 31	wa	$wff ((x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v))$
33	32 1 2	copab	$class \{⟨x, y⟩ \| ((x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v))\}$
34	0 33	wceq	$wff ~_{𝑹} = \{⟨x, y⟩ \| ((x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v))\}$

Metamath Proof Explorer

Definition df-enr

Detailed syntax breakdown