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

Theorem elpqn 9707
 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 9694 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
2 ssrab2 3672 . . 3 {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))} ⊆ (N × N)
31, 2eqsstri 3620 . 2 Q ⊆ (N × N)
43sseli 3584 1 (𝐴Q𝐴 ∈ (N × N))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1987  ∀wral 2908  {crab 2912   class class class wbr 4623   × cxp 5082  ‘cfv 5857  2nd c2nd 7127  Ncnpi 9626
 Copyright terms: Public domain W3C validator