![]() |
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 10075 | . 2 ⊢ <Q = ( <pQ ∩ (Q × Q)) | |
2 | inss2 4054 | . 2 ⊢ ( <pQ ∩ (Q × Q)) ⊆ (Q × Q) | |
3 | 1, 2 | eqsstri 3854 | 1 ⊢ <Q ⊆ (Q × Q) |
Colors of variables: wff setvar class |
Syntax hints: ∩ cin 3791 ⊆ wss 3792 × cxp 5353 <pQ cltpq 10007 Qcnq 10009 <Q cltq 10015 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-in 3799 df-ss 3806 df-ltnq 10075 |
This theorem is referenced by: lterpq 10127 ltanq 10128 ltmnq 10129 ltexnq 10132 ltbtwnnq 10135 ltrnq 10136 prcdnq 10150 prnmadd 10154 genpcd 10163 nqpr 10171 1idpr 10186 prlem934 10190 ltexprlem4 10196 prlem936 10204 reclem2pr 10205 reclem3pr 10206 reclem4pr 10207 |
Copyright terms: Public domain | W3C validator |