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

Theorem dtru 4682
Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Note that we may not substitute the same variable for both 𝑥 and 𝑦 (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 1907.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2494 or ax-sep 4607. See dtruALT 4725 for a shorter proof using these axioms.

The proof makes use of dummy variables 𝑧 and 𝑤 which do not appear in the final theorem. They must be distinct from each other and from 𝑥 and 𝑦. In other words, if we were to substitute 𝑥 for 𝑧 throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006.)

Assertion
Ref Expression
dtru ¬ ∀𝑥 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem dtru
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 el 4672 . . . 4 𝑤 𝑥𝑤
2 ax-nul 4616 . . . . 5 𝑧𝑥 ¬ 𝑥𝑧
3 sp 1990 . . . . 5 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
42, 3eximii 1742 . . . 4 𝑧 ¬ 𝑥𝑧
5 eeanv 2125 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
61, 4, 5mpbir2an 956 . . 3 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
7 ax9 1951 . . . . . 6 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
87com12 32 . . . . 5 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
98con3dimp 455 . . . 4 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
1092eximi 1741 . . 3 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
11 equequ2 1903 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1211notbid 306 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
13 ax7 1893 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1413con3d 146 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1514spimev 2150 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1612, 15syl6bi 241 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
17 ax7 1893 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1817con3d 146 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
1918spimev 2150 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2019a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2116, 20pm2.61i 174 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2221exlimivv 1813 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
236, 10, 22mp2b 10 . 2 𝑥 ¬ 𝑥 = 𝑦
24 exnal 1732 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2523, 24mpbi 218 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-nul 4616  ax-pow 4668
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699
This theorem is referenced by:  axc16b  4683  eunex  4684  nfnid  4722  dtrucor  4726  dvdemo1  4728  brprcneu  5979  zfcndpow  9192
  Copyright terms: Public domain W3C validator