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

Theorem vn0 4351
Description: The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.) Avoid ax-8 2108, df-clel 2814. (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 1551 . . . . . . 7 ¬ ⊥
2 pm5.501 366 . . . . . . . 8 (⊤ → (⊥ ↔ (⊤ ↔ ⊥)))
32mptru 1544 . . . . . . 7 (⊥ ↔ (⊤ ↔ ⊥))
41, 3mtbi 322 . . . . . 6 ¬ (⊤ ↔ ⊥)
54exgen 1972 . . . . 5 𝑦 ¬ (⊤ ↔ ⊥)
6 exnal 1824 . . . . 5 (∃𝑦 ¬ (⊤ ↔ ⊥) ↔ ¬ ∀𝑦(⊤ ↔ ⊥))
75, 6mpbi 230 . . . 4 ¬ ∀𝑦(⊤ ↔ ⊥)
8 df-clab 2713 . . . . . . 7 (𝑦 ∈ {𝑥 ∣ ⊤} ↔ [𝑦 / 𝑥]⊤)
9 sbv 2086 . . . . . . 7 ([𝑦 / 𝑥]⊤ ↔ ⊤)
108, 9bitr2i 276 . . . . . 6 (⊤ ↔ 𝑦 ∈ {𝑥 ∣ ⊤})
11 df-clab 2713 . . . . . . 7 (𝑦 ∈ {𝑥 ∣ ⊥} ↔ [𝑦 / 𝑥]⊥)
12 sbv 2086 . . . . . . 7 ([𝑦 / 𝑥]⊥ ↔ ⊥)
1311, 12bitr2i 276 . . . . . 6 (⊥ ↔ 𝑦 ∈ {𝑥 ∣ ⊥})
1410, 13bibi12i 339 . . . . 5 ((⊤ ↔ ⊥) ↔ (𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}))
1514albii 1816 . . . 4 (∀𝑦(⊤ ↔ ⊥) ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}))
167, 15mtbi 322 . . 3 ¬ ∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥})
17 dfcleq 2728 . . . 4 ({𝑥 ∣ ⊤} = {𝑥 ∣ ⊥} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}))
18 dfv2 3481 . . . . . 6 V = {𝑥 ∣ ⊤}
1918eqcomi 2744 . . . . 5 {𝑥 ∣ ⊤} = V
20 dfnul4 4341 . . . . . 6 ∅ = {𝑥 ∣ ⊥}
2120eqcomi 2744 . . . . 5 {𝑥 ∣ ⊥} = ∅
2219, 21eqeq12i 2753 . . . 4 ({𝑥 ∣ ⊤} = {𝑥 ∣ ⊥} ↔ V = ∅)
2317, 22bitr3i 277 . . 3 (∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}) ↔ V = ∅)
2416, 23mtbi 322 . 2 ¬ V = ∅
2524neir 2941 1 V ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1535   = wceq 1537  wtru 1538  wfal 1549  wex 1776  [wsb 2062  wcel 2106  {cab 2712  wne 2938  Vcvv 3478  c0 4339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-ne 2939  df-v 3480  df-dif 3966  df-nul 4340
This theorem is referenced by:  uniintsn  4990  relrelss  6295  imasaddfnlem  17575  imasvscafn  17584  cmpfi  23432  fclscmp  24054  zarcmplem  33842  compne  44437
  Copyright terms: Public domain W3C validator