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

Theorem 0nnq 9947
 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.)
Assertion
Ref Expression
0nnq ¬ ∅ ∈ Q

Proof of Theorem 0nnq
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef 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)
42, 3eqsstri 3782 . . 3 Q ⊆ (N × N)
54sseli 3746 . 2 (∅ ∈ Q → ∅ ∈ (N × N))
61, 5mto 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
 Copyright terms: Public domain W3C validator