df-enq

Description: Define equivalence relation for positive fractions. 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-2.1 of Gleason p. 117. (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-enq	$⊢ ~_{𝑸} = \{⟨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 \cdot_{𝑵} u = w \cdot_{𝑵} v))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceq	$class ~_{𝑸}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cnpi	$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		cmi	$class \cdot_{𝑵}$
24	14 19 23	co	$class (z \cdot_{𝑵} u)$
25	15 18 23	co	$class (w \cdot_{𝑵} v)$
26	24 25	wceq	$wff z \cdot_{𝑵} u = w \cdot_{𝑵} v$
27	22 26	wa	$wff ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \cdot_{𝑵} u = w \cdot_{𝑵} v)$
28	27 13	wex	$wff \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \cdot_{𝑵} u = w \cdot_{𝑵} v)$
29	28 12	wex	$wff \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \cdot_{𝑵} u = w \cdot_{𝑵} v)$
30	29 11	wex	$wff \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \cdot_{𝑵} u = w \cdot_{𝑵} v)$
31	30 10	wex	$wff \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \cdot_{𝑵} u = w \cdot_{𝑵} 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 \cdot_{𝑵} u = w \cdot_{𝑵} 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 \cdot_{𝑵} u = w \cdot_{𝑵} 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 \cdot_{𝑵} u = w \cdot_{𝑵} v))\}$

Metamath Proof Explorer

Definition df-enq

Detailed syntax breakdown