Definition df-enq0 7491

Description: Define equivalence relation for nonnegative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)

Assertion

Ref	Expression
df-enq0	|- ~Q0 = { <. x , y >. | ( ( x e. ( om X. N. ) /\ y e. ( om X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) ) ) }

Distinct variable group:   x, y, z, w, v, u

Detailed syntax breakdown of Definition df-enq0

Step	Hyp	Ref	Expression
1		ceq0 7353	. 2 class ~Q0
2		vx	. . . . . . 7 setvar x
3	2	cv 1363	. . . . . 6 class x
4		com 4626	. . . . . . 7 class om
5		cnpi 7339	. . . . . . 7 class N.
6	4, 5	cxp 4661	. . . . . 6 class ( om X. N. )
7	3, 6	wcel 2167	. . . . 5 wff x e. ( om X. N. )
8		vy	. . . . . . 7 setvar y
9	8	cv 1363	. . . . . 6 class y
10	9, 6	wcel 2167	. . . . 5 wff y e. ( om X. N. )
11	7, 10	wa 104	. . . 4 wff ( x e. ( om X. N. ) /\ y e. ( om X. N. ) )
12		vz	. . . . . . . . . . . . 13 setvar z
13	12	cv 1363	. . . . . . . . . . . 12 class z
14		vw	. . . . . . . . . . . . 13 setvar w
15	14	cv 1363	. . . . . . . . . . . 12 class w
16	13, 15	cop 3625	. . . . . . . . . . 11 class <. z , w >.
17	3, 16	wceq 1364	. . . . . . . . . 10 wff x = <. z , w >.
18		vv	. . . . . . . . . . . . 13 setvar v
19	18	cv 1363	. . . . . . . . . . . 12 class v
20		vu	. . . . . . . . . . . . 13 setvar u
21	20	cv 1363	. . . . . . . . . . . 12 class u
22	19, 21	cop 3625	. . . . . . . . . . 11 class <. v , u >.
23	9, 22	wceq 1364	. . . . . . . . . 10 wff y = <. v , u >.
24	17, 23	wa 104	. . . . . . . . 9 wff ( x = <. z , w >. /\ y = <. v , u >. )
25		comu 6472	. . . . . . . . . . 11 class .o
26	13, 21, 25	co 5922	. . . . . . . . . 10 class ( z .o u )
27	15, 19, 25	co 5922	. . . . . . . . . 10 class ( w .o v )
28	26, 27	wceq 1364	. . . . . . . . 9 wff ( z .o u ) = ( w .o v )
29	24, 28	wa 104	. . . . . . . 8 wff ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) )
30	29, 20	wex 1506	. . . . . . 7 wff E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) )
31	30, 18	wex 1506	. . . . . 6 wff E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) )
32	31, 14	wex 1506	. . . . 5 wff E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) )
33	32, 12	wex 1506	. . . 4 wff E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) )
34	11, 33	wa 104	. . 3 wff ( ( x e. ( om X. N. ) /\ y e. ( om X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) ) )
35	34, 2, 8	copab 4093	. 2 class { <. x , y >. | ( ( x e. ( om X. N. ) /\ y e. ( om X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) ) ) }
36	1, 35	wceq 1364	1 wff ~Q0 = { <. x , y >. | ( ( x e. ( om X. N. ) /\ y e. ( om X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .o u ) = ( w .o v ) ) ) }

This definition is referenced by:  enq0enq  7498  enq0sym  7499  enq0ref  7500  enq0tr  7501  enq0er  7502  enq0breq  7503  enq0ex  7506