Theorem enqex 7263

Description: The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)

Assertion

Ref	Expression
enqex	|- ~Q e. _V

Proof of Theorem enqex

Dummy variables x y z w v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		niex 7215	. . . 4 |- N. e. _V
2	1, 1	xpex 4698	. . 3 |- ( N. X. N. ) e. _V
3	2, 2	xpex 4698	. 2 |- ( ( N. X. N. ) X. ( N. X. N. ) ) e. _V
4		df-enq 7250	. . 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 ) ) ) }
5		opabssxp 4657	. . 3 |- { <. 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 ) ) ) } C_ ( ( N. X. N. ) X. ( N. X. N. ) )
6	4, 5	eqsstri 3160	. 2 |- ~Q C_ ( ( N. X. N. ) X. ( N. X. N. ) )
7	3, 6	ssexi 4102	1 |- ~Q e. _V

Syntax hints:   /\ wa 103   = wceq 1335   E.wex 1472   e. wcel 2128   _Vcvv 2712   <.cop 3563   {copab 4024   X. cxp 4581  (class class class)co 5818   N.cnpi 7175   .N cmi 7177   ~Q ceq 7182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-iinf 4545

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-opab 4026  df-iom 4548  df-xp 4589  df-ni 7207  df-enq 7250

This theorem is referenced by:  1nq  7269  addpipqqs  7273  mulpipqqs  7276  ordpipqqs  7277  addclnq  7278  mulclnq  7279  dmaddpq  7282  dmmulpq  7283  recexnq  7293  ltexnqq  7311  prarloclemarch  7321  prarloclemarch2  7322  nnnq  7325  nqpnq0nq  7356  prarloclemlt  7396  prarloclemlo  7397  prarloclemcalc  7405  nqprm  7445