Metamath Proof Explorer

Definition 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 ∈ 𝑵 × 𝑵 ∧ y ∈ 𝑵 × 𝑵 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 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 𝑵 × 𝑵
6 3 5 wcel wff x ∈ 𝑵 × 𝑵
7 2 cv setvar y
8 7 5 wcel wff y ∈ 𝑵 × 𝑵
9 6 8 wa wff x ∈ 𝑵 × 𝑵 ∧ y ∈ 𝑵 × 𝑵
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 ∧ y = v u
23 cmi 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 ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v
28 27 13 wex wff ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v
29 28 12 wex wff ∃ v ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v
30 29 11 wex wff ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v
31 30 10 wex wff ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v
32 9 31 wa wff x ∈ 𝑵 × 𝑵 ∧ y ∈ 𝑵 × 𝑵 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v
33 32 1 2 copab class x y | x ∈ 𝑵 × 𝑵 ∧ y ∈ 𝑵 × 𝑵 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v
34 0 33 wceq wff ~ 𝑸 = x y | x ∈ 𝑵 × 𝑵 ∧ y ∈ 𝑵 × 𝑵 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ∧ y = v u ∧ z ⋅ 𝑵 u = w ⋅ 𝑵 v