ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  enq0enq Unicode version

Theorem enq0enq 6587
Description: Equivalence on positive fractions in terms of equivalence on non-negative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.)
Assertion
Ref Expression
enq0enq  |-  ~Q  =  ( ~Q0  i^i  ( ( N.  X.  N. )  X.  ( N.  X.  N. ) ) )

Proof of Theorem enq0enq
Dummy variables  v  u  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-enq0 6580 . . 3  |- ~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 ) ) ) }
2 df-xp 4379 . . 3  |-  ( ( N.  X.  N. )  X.  ( N.  X.  N. ) )  =  { <. x ,  y >.  |  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
) }
31, 2ineq12i 3164 . 2  |-  ( ~Q0  i^i  (
( N.  X.  N. )  X.  ( N.  X.  N. ) ) )  =  ( { <. 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 ) ) ) }  i^i  { <. x ,  y >.  |  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
) } )
4 inopab 4496 . 2  |-  ( {
<. 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 ) ) ) }  i^i  { <. x ,  y >.  |  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
) } )  =  { <. 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 ) ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) ) }
5 an32 504 . . . . . 6  |-  ( ( ( ( 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 ) ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  <->  ( (
( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  ( 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  .o  u
)  =  ( w  .o  v ) ) ) )
6 an4 528 . . . . . . . 8  |-  ( ( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
) )  <->  ( (
x  e.  ( om 
X.  N. )  /\  x  e.  ( N.  X.  N. ) )  /\  (
y  e.  ( om 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) ) )
7 pinn 6465 . . . . . . . . . . . . 13  |-  ( x  e.  N.  ->  x  e.  om )
87ssriv 2977 . . . . . . . . . . . 12  |-  N.  C_  om
9 xpss1 4476 . . . . . . . . . . . 12  |-  ( N.  C_  om  ->  ( N.  X.  N. )  C_  ( om  X.  N. ) )
108, 9ax-mp 7 . . . . . . . . . . 11  |-  ( N. 
X.  N. )  C_  ( om  X.  N. )
1110sseli 2969 . . . . . . . . . 10  |-  ( x  e.  ( N.  X.  N. )  ->  x  e.  ( om  X.  N. ) )
1211pm4.71ri 378 . . . . . . . . 9  |-  ( x  e.  ( N.  X.  N. )  <->  ( x  e.  ( om  X.  N. )  /\  x  e.  ( N.  X.  N. )
) )
1310sseli 2969 . . . . . . . . . 10  |-  ( y  e.  ( N.  X.  N. )  ->  y  e.  ( om  X.  N. ) )
1413pm4.71ri 378 . . . . . . . . 9  |-  ( y  e.  ( N.  X.  N. )  <->  ( y  e.  ( om  X.  N. )  /\  y  e.  ( N.  X.  N. )
) )
1512, 14anbi12i 441 . . . . . . . 8  |-  ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  <->  ( (
x  e.  ( om 
X.  N. )  /\  x  e.  ( N.  X.  N. ) )  /\  (
y  e.  ( om 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) ) )
166, 15bitr4i 180 . . . . . . 7  |-  ( ( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
) )  <->  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
) )
1716anbi1i 439 . . . . . 6  |-  ( ( ( ( x  e.  ( om  X.  N. )  /\  y  e.  ( om  X.  N. )
)  /\  ( 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  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( 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  .o  u
)  =  ( w  .o  v ) ) ) )
185, 17bitri 177 . . . . 5  |-  ( ( ( ( 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 ) ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  <->  ( (
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  .o  u
)  =  ( w  .o  v ) ) ) )
19 eleq1 2116 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  <. z ,  w >.  ->  ( x  e.  ( N.  X.  N. ) 
<-> 
<. z ,  w >.  e.  ( N.  X.  N. ) ) )
20 opelxp 4402 . . . . . . . . . . . . . . . . . . 19  |-  ( <.
z ,  w >.  e.  ( N.  X.  N. ) 
<->  ( z  e.  N.  /\  w  e.  N. )
)
2119, 20syl6bb 189 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  <. z ,  w >.  ->  ( x  e.  ( N.  X.  N. ) 
<->  ( z  e.  N.  /\  w  e.  N. )
) )
22 eleq1 2116 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  <. v ,  u >.  ->  ( y  e.  ( N.  X.  N. ) 
<-> 
<. v ,  u >.  e.  ( N.  X.  N. ) ) )
23 opelxp 4402 . . . . . . . . . . . . . . . . . . 19  |-  ( <.
v ,  u >.  e.  ( N.  X.  N. ) 
<->  ( v  e.  N.  /\  u  e.  N. )
)
2422, 23syl6bb 189 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  <. v ,  u >.  ->  ( y  e.  ( N.  X.  N. ) 
<->  ( v  e.  N.  /\  u  e.  N. )
) )
2521, 24bi2anan9 548 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  ->  ( (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  <->  ( (
z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
) ) )
2625pm5.32i 435 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  <->  ( (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
) ) )
2726anbi1i 439 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  <-> 
( ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( z  e. 
N.  /\  w  e.  N. )  /\  (
v  e.  N.  /\  u  e.  N. )
) )  /\  (
z  .o  u )  =  ( w  .o  v ) ) )
28 anass 387 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
) )  /\  (
z  .o  u )  =  ( w  .o  v ) )  <->  ( (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .o  u )  =  ( w  .o  v ) ) ) )
2927, 28bitri 177 . . . . . . . . . . . . . 14  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  <-> 
( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
( ( z  e. 
N.  /\  w  e.  N. )  /\  (
v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .o  u )  =  ( w  .o  v ) ) ) )
30 mulpiord 6473 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  N.  /\  u  e.  N. )  ->  ( z  .N  u
)  =  ( z  .o  u ) )
31 mulpiord 6473 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  e.  N.  /\  v  e.  N. )  ->  ( w  .N  v
)  =  ( w  .o  v ) )
3230, 31eqeqan12d 2071 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  N.  /\  u  e.  N. )  /\  ( w  e.  N.  /\  v  e.  N. )
)  ->  ( (
z  .N  u )  =  ( w  .N  v )  <->  ( z  .o  u )  =  ( w  .o  v ) ) )
3332an42s 531 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  ->  ( (
z  .N  u )  =  ( w  .N  v )  <->  ( z  .o  u )  =  ( w  .o  v ) ) )
3433pm5.32i 435 . . . . . . . . . . . . . . 15  |-  ( ( ( ( z  e. 
N.  /\  w  e.  N. )  /\  (
v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .N  u )  =  ( w  .N  v ) )  <->  ( ( ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .o  u )  =  ( w  .o  v ) ) )
3534anbi2i 438 . . . . . . . . . . . . . 14  |-  ( ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .N  u )  =  ( w  .N  v ) ) )  <->  ( (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .o  u )  =  ( w  .o  v ) ) ) )
3629, 35bitr4i 180 . . . . . . . . . . . . 13  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  <-> 
( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
( ( z  e. 
N.  /\  w  e.  N. )  /\  (
v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .N  u )  =  ( w  .N  v ) ) ) )
37 anass 387 . . . . . . . . . . . . 13  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
) )  /\  (
z  .N  u )  =  ( w  .N  v ) )  <->  ( (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( ( z  e.  N.  /\  w  e.  N. )  /\  ( v  e.  N.  /\  u  e.  N. )
)  /\  ( z  .N  u )  =  ( w  .N  v ) ) ) )
3836, 37bitr4i 180 . . . . . . . . . . . 12  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  <-> 
( ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( z  e. 
N.  /\  w  e.  N. )  /\  (
v  e.  N.  /\  u  e.  N. )
) )  /\  (
z  .N  u )  =  ( w  .N  v ) ) )
3926anbi1i 439 . . . . . . . . . . . 12  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .N  u
)  =  ( w  .N  v ) )  <-> 
( ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( ( z  e. 
N.  /\  w  e.  N. )  /\  (
v  e.  N.  /\  u  e.  N. )
) )  /\  (
z  .N  u )  =  ( w  .N  v ) ) )
4038, 39bitr4i 180 . . . . . . . . . . 11  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  <-> 
( ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .N  u )  =  ( w  .N  v
) ) )
41 ancom 257 . . . . . . . . . . . 12  |-  ( ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  <->  ( (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. ) ) )
4241anbi1i 439 . . . . . . . . . . 11  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .o  u
)  =  ( w  .o  v ) )  <-> 
( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. ) )  /\  (
z  .o  u )  =  ( w  .o  v ) ) )
4341anbi1i 439 . . . . . . . . . . 11  |-  ( ( ( ( x  = 
<. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  (
x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  /\  ( z  .N  u
)  =  ( w  .N  v ) )  <-> 
( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. ) )  /\  (
z  .N  u )  =  ( w  .N  v ) ) )
4440, 42, 433bitr3i 203 . . . . . . . . . 10  |-  ( ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )
)  /\  ( z  .o  u )  =  ( w  .o  v ) )  <->  ( ( ( x  e.  ( N. 
X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. ) )  /\  (
z  .N  u )  =  ( w  .N  v ) ) )
45 anass 387 . . . . . . . . . 10  |-  ( ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )
)  /\  ( z  .o  u )  =  ( w  .o  v ) )  <->  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) ) ) )
46 anass 387 . . . . . . . . . 10  |-  ( ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )
)  /\  ( z  .N  u )  =  ( w  .N  v ) )  <->  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u )  =  ( w  .N  v
) ) ) )
4744, 45, 463bitr3i 203 . . . . . . . . 9  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  (
( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u )  =  ( w  .N  v
) ) ) )
48472exbii 1513 . . . . . . . 8  |-  ( E. v E. u ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  E. v E. u
( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  ( (
x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u )  =  ( w  .N  v
) ) ) )
49 19.42vv 1804 . . . . . . . 8  |-  ( E. v E. u ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u )  =  ( w  .o  v
) ) ) )
50 19.42vv 1804 . . . . . . . 8  |-  ( E. v E. u ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u
)  =  ( w  .N  v ) ) )  <->  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u )  =  ( w  .N  v
) ) ) )
5148, 49, 503bitr3i 203 . . . . . . 7  |-  ( ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u )  =  ( w  .N  v
) ) ) )
52512exbii 1513 . . . . . 6  |-  ( E. z E. w ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  E. z E. w
( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. )
)  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u
)  =  ( w  .N  v ) ) ) )
53 19.42vv 1804 . . . . . 6  |-  ( E. z E. w ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( 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  .o  u
)  =  ( w  .o  v ) ) ) )
54 19.42vv 1804 . . . . . 6  |-  ( E. z E. w ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u
)  =  ( w  .N  v ) ) )  <->  ( ( 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 ) ) ) )
5552, 53, 543bitr3i 203 . . . . 5  |-  ( ( ( 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  .o  u
)  =  ( w  .o  v ) ) )  <->  ( ( 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 ) ) ) )
5618, 55bitri 177 . . . 4  |-  ( ( ( ( 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 ) ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) )  <->  ( (
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 ) ) ) )
5756opabbii 3852 . . 3  |-  { <. 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 ) ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) ) }  =  { <. 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 ) ) ) }
58 df-enq 6503 . . 3  |-  ~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 ) ) ) }
5957, 58eqtr4i 2079 . 2  |-  { <. 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 ) ) )  /\  ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) ) }  =  ~Q
603, 4, 593eqtrri 2081 1  |-  ~Q  =  ( ~Q0  i^i  ( ( N.  X.  N. )  X.  ( N.  X.  N. ) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 101    <-> wb 102    = wceq 1259   E.wex 1397    e. wcel 1409    i^i cin 2944    C_ wss 2945   <.cop 3406   {copab 3845   omcom 4341    X. cxp 4371  (class class class)co 5540    .o comu 6030   N.cnpi 6428    .N cmi 6430    ~Q ceq 6435   ~Q0 ceq0 6442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-pow 3955  ax-pr 3972
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-dif 2948  df-un 2950  df-in 2952  df-ss 2959  df-pw 3389  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-opab 3847  df-xp 4379  df-rel 4380  df-res 4385  df-iota 4895  df-fv 4938  df-ov 5543  df-ni 6460  df-mi 6462  df-enq 6503  df-enq0 6580
This theorem is referenced by:  nqnq0pi  6594
  Copyright terms: Public domain W3C validator