![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltrelnq | Structured version Visualization version GIF version |
Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ltrelnq | ⊢ <Q ⊆ (Q × Q) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ltnq 10943 | . 2 ⊢ <Q = ( <pQ ∩ (Q × Q)) | |
2 | inss2 4228 | . 2 ⊢ ( <pQ ∩ (Q × Q)) ⊆ (Q × Q) | |
3 | 1, 2 | eqsstri 4011 | 1 ⊢ <Q ⊆ (Q × Q) |
Colors of variables: wff setvar class |
Syntax hints: ∩ cin 3943 ⊆ wss 3944 × cxp 5676 <pQ cltpq 10875 Qcnq 10877 <Q cltq 10883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-in 3951 df-ss 3961 df-ltnq 10943 |
This theorem is referenced by: lterpq 10995 ltanq 10996 ltmnq 10997 ltexnq 11000 ltbtwnnq 11003 ltrnq 11004 prcdnq 11018 prnmadd 11022 genpcd 11031 nqpr 11039 1idpr 11054 prlem934 11058 ltexprlem4 11064 prlem936 11072 reclem2pr 11073 reclem3pr 11074 reclem4pr 11075 |
Copyright terms: Public domain | W3C validator |