Theorem enqex 7326

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

Assertion

Ref	Expression
enqex	⊢ ~Q ∈ V

Proof of Theorem enqex

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		niex 7278	. . . 4 ⊢ N ∈ V
2	1, 1	xpex 4727	. . 3 ⊢ (N × N) ∈ V
3	2, 2	xpex 4727	. 2 ⊢ ((N × N) × (N × N)) ∈ V
4		df-enq 7313	. . 3 ⊢ ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
5		opabssxp 4686	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} ⊆ ((N × N) × (N × N))
6	4, 5	eqsstri 3180	. 2 ⊢ ~Q ⊆ ((N × N) × (N × N))
7	3, 6	ssexi 4128	1 ⊢ ~Q ∈ V

Syntax hints:   ∧ wa 103   = wceq 1349  ∃wex 1486   ∈ wcel 2142  Vcvv 2731  ⟨cop 3587  {copab 4050   × cxp 4610  (class class class)co 5857  Ncnpi 7238   ·_N cmi 7240   ~_Q ceq 7245

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 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-iinf 4573

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-opab 4052  df-iom 4576  df-xp 4618  df-ni 7270  df-enq 7313

This theorem is referenced by:  1nq  7332  addpipqqs  7336  mulpipqqs  7339  ordpipqqs  7340  addclnq  7341  mulclnq  7342  dmaddpq  7345  dmmulpq  7346  recexnq  7356  ltexnqq  7374  prarloclemarch  7384  prarloclemarch2  7385  nnnq  7388  nqpnq0nq  7419  prarloclemlt  7459  prarloclemlo  7460  prarloclemcalc  7468  nqprm  7508