 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpqn Structured version   Visualization version   GIF version

Theorem elpqn 9626
 Description: Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
elpqn (𝐴Q𝐴 ∈ (N × N))

Proof of Theorem elpqn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nq 9613 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
2 ssrab2 3650 . . 3 {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))} ⊆ (N × N)
31, 2eqsstri 3598 . 2 Q ⊆ (N × N)
43sseli 3564 1 (𝐴Q𝐴 ∈ (N × N))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1977  ∀wral 2896  {crab 2900   class class class wbr 4583   × cxp 5036  ‘cfv 5804  2nd c2nd 7058  Ncnpi 9545
 Copyright terms: Public domain W3C validator