|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > elpqn | Structured version Visualization version GIF version | ||
| 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.) | 
| Ref | Expression | 
|---|---|
| elpqn | ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-nq 10953 | . . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} | |
| 2 | 1 | ssrab3 4081 | . 2 ⊢ Q ⊆ (N × N) | 
| 3 | 2 | sseli 3978 | 1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2107 ∀wral 3060 class class class wbr 5142 × cxp 5682 ‘cfv 6560 2nd c2nd 8014 Ncnpi 10885 <N clti 10888 ~Q ceq 10892 Qcnq 10893 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-ss 3967 df-nq 10953 | 
| This theorem is referenced by: nqereu 10970 nqerid 10974 enqeq 10975 addpqnq 10979 mulpqnq 10982 ordpinq 10984 addclnq 10986 mulclnq 10988 addnqf 10989 mulnqf 10990 adderpq 10997 mulerpq 10998 addassnq 10999 mulassnq 11000 distrnq 11002 mulidnq 11004 recmulnq 11005 ltsonq 11010 lterpq 11011 ltanq 11012 ltmnq 11013 ltexnq 11016 archnq 11021 wuncn 11211 | 
| Copyright terms: Public domain | W3C validator |