![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0nnq | Structured version Visualization version GIF version |
Description: The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
0nnq | ⊢ ¬ ∅ ∈ Q |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0nelxp 5283 | . 2 ⊢ ¬ ∅ ∈ (N × N) | |
2 | df-nq 9935 | . . . 4 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} | |
3 | ssrab2 3834 | . . . 4 ⊢ {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} ⊆ (N × N) | |
4 | 2, 3 | eqsstri 3782 | . . 3 ⊢ Q ⊆ (N × N) |
5 | 4 | sseli 3746 | . 2 ⊢ (∅ ∈ Q → ∅ ∈ (N × N)) |
6 | 1, 5 | mto 188 | 1 ⊢ ¬ ∅ ∈ Q |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2144 ∀wral 3060 {crab 3064 ∅c0 4061 class class class wbr 4784 × cxp 5247 ‘cfv 6031 2nd c2nd 7313 Ncnpi 9867 <N clti 9870 ~Q ceq 9874 Qcnq 9875 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-sep 4912 ax-nul 4920 ax-pr 5034 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ne 2943 df-rab 3069 df-v 3351 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-sn 4315 df-pr 4317 df-op 4321 df-opab 4845 df-xp 5255 df-nq 9935 |
This theorem is referenced by: adderpq 9979 mulerpq 9980 addassnq 9981 mulassnq 9982 distrnq 9984 recmulnq 9987 recclnq 9989 ltanq 9994 ltmnq 9995 ltexnq 9998 nsmallnq 10000 ltbtwnnq 10001 ltrnq 10002 prlem934 10056 ltaddpr 10057 ltexprlem2 10060 ltexprlem3 10061 ltexprlem4 10062 ltexprlem6 10064 ltexprlem7 10065 prlem936 10070 reclem2pr 10071 |
Copyright terms: Public domain | W3C validator |