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 
|- ~Q = { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceq 
 |-  ~Q
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 cnpi 
 |-  N.
5 4 4 cxp 
 |-  ( N. X. N. )
6 3 5 wcel 
 |-  x e. ( N. X. N. )
7 2 cv 
 |-  y
8 7 5 wcel 
 |-  y e. ( N. X. N. )
9 6 8 wa 
 |-  ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) )
10 vz 
 |-  z
11 vw 
 |-  w
12 vv 
 |-  v
13 vu 
 |-  u
14 10 cv 
 |-  z
15 11 cv 
 |-  w
16 14 15 cop 
 |-  <. z , w >.
17 3 16 wceq 
 |-  x = <. z , w >.
18 12 cv 
 |-  v
19 13 cv 
 |-  u
20 18 19 cop 
 |-  <. v , u >.
21 7 20 wceq 
 |-  y = <. v , u >.
22 17 21 wa 
 |-  ( x = <. z , w >. /\ y = <. v , u >. )
23 cmi 
 |-  .N
24 14 19 23 co 
 |-  ( z .N u )
25 15 18 23 co 
 |-  ( w .N v )
26 24 25 wceq 
 |-  ( z .N u ) = ( w .N v )
27 22 26 wa 
 |-  ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) )
28 27 13 wex 
 |-  E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) )
29 28 12 wex 
 |-  E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) )
30 29 11 wex 
 |-  E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) )
31 30 10 wex 
 |-  E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) )
32 9 31 wa 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) ) )
33 32 1 2 copab 
 |-  { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) ) ) }
34 0 33 wceq 
 |-  ~Q = { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) ) ) }