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

Theorem vn0 4344
Description: The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.) Avoid ax-8 2109, df-clel 2815. (Revised by GG, 6-Sep-2024.)
Assertion
Ref Expression
vn0 V ≠ ∅

Proof of Theorem vn0
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fal 1553 . . . . . . 7 ¬ ⊥
2 pm5.501 366 . . . . . . . 8 (⊤ → (⊥ ↔ (⊤ ↔ ⊥)))
32mptru 1546 . . . . . . 7 (⊥ ↔ (⊤ ↔ ⊥))
41, 3mtbi 322 . . . . . 6 ¬ (⊤ ↔ ⊥)
54exgen 1973 . . . . 5 𝑦 ¬ (⊤ ↔ ⊥)
6 exnal 1826 . . . . 5 (∃𝑦 ¬ (⊤ ↔ ⊥) ↔ ¬ ∀𝑦(⊤ ↔ ⊥))
75, 6mpbi 230 . . . 4 ¬ ∀𝑦(⊤ ↔ ⊥)
8 df-clab 2714 . . . . . . 7 (𝑦 ∈ {𝑥 ∣ ⊤} ↔ [𝑦 / 𝑥]⊤)
9 sbv 2087 . . . . . . 7 ([𝑦 / 𝑥]⊤ ↔ ⊤)
108, 9bitr2i 276 . . . . . 6 (⊤ ↔ 𝑦 ∈ {𝑥 ∣ ⊤})
11 df-clab 2714 . . . . . . 7 (𝑦 ∈ {𝑥 ∣ ⊥} ↔ [𝑦 / 𝑥]⊥)
12 sbv 2087 . . . . . . 7 ([𝑦 / 𝑥]⊥ ↔ ⊥)
1311, 12bitr2i 276 . . . . . 6 (⊥ ↔ 𝑦 ∈ {𝑥 ∣ ⊥})
1410, 13bibi12i 339 . . . . 5 ((⊤ ↔ ⊥) ↔ (𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}))
1514albii 1818 . . . 4 (∀𝑦(⊤ ↔ ⊥) ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}))
167, 15mtbi 322 . . 3 ¬ ∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥})
17 dfcleq 2729 . . . 4 ({𝑥 ∣ ⊤} = {𝑥 ∣ ⊥} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}))
18 dfv2 3482 . . . . . 6 V = {𝑥 ∣ ⊤}
1918eqcomi 2745 . . . . 5 {𝑥 ∣ ⊤} = V
20 dfnul4 4334 . . . . . 6 ∅ = {𝑥 ∣ ⊥}
2120eqcomi 2745 . . . . 5 {𝑥 ∣ ⊥} = ∅
2219, 21eqeq12i 2754 . . . 4 ({𝑥 ∣ ⊤} = {𝑥 ∣ ⊥} ↔ V = ∅)
2317, 22bitr3i 277 . . 3 (∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}) ↔ V = ∅)
2416, 23mtbi 322 . 2 ¬ V = ∅
2524neir 2942 1 V ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1537   = wceq 1539  wtru 1540  wfal 1551  wex 1778  [wsb 2063  wcel 2107  {cab 2713  wne 2939  Vcvv 3479  c0 4332
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-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-ne 2940  df-v 3481  df-dif 3953  df-nul 4333
This theorem is referenced by:  uniintsn  4984  relrelss  6292  imasaddfnlem  17574  imasvscafn  17583  cmpfi  23417  fclscmp  24039  zarcmplem  33881  compne  44465
  Copyright terms: Public domain W3C validator