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

Theorem elpqn 9732
 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 9719 . . 3 Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))}
2 ssrab2 3679 . . 3 {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))} ⊆ (N × N)
31, 2eqsstri 3627 . 2 Q ⊆ (N × N)
43sseli 3591 1 (𝐴Q𝐴 ∈ (N × N))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1988  ∀wral 2909  {crab 2913   class class class wbr 4644   × cxp 5102  ‘cfv 5876  2nd c2nd 7152  Ncnpi 9651
 Copyright terms: Public domain W3C validator