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

Theorem dtru 5070
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 2132.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2803 or ax-sep 5005. See dtruALT 5087 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 5069 . . . 4 𝑤 𝑥𝑤
2 ax-nul 5013 . . . . 5 𝑧𝑥 ¬ 𝑥𝑧
3 sp 2224 . . . . 5 (∀𝑥 ¬ 𝑥𝑧 → ¬ 𝑥𝑧)
42, 3eximii 1935 . . . 4 𝑧 ¬ 𝑥𝑧
5 exdistrv 2054 . . . 4 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) ↔ (∃𝑤 𝑥𝑤 ∧ ∃𝑧 ¬ 𝑥𝑧))
61, 4, 5mpbir2an 702 . . 3 𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧)
7 ax9 2177 . . . . . 6 (𝑤 = 𝑧 → (𝑥𝑤𝑥𝑧))
87com12 32 . . . . 5 (𝑥𝑤 → (𝑤 = 𝑧𝑥𝑧))
98con3dimp 399 . . . 4 ((𝑥𝑤 ∧ ¬ 𝑥𝑧) → ¬ 𝑤 = 𝑧)
1092eximi 1934 . . 3 (∃𝑤𝑧(𝑥𝑤 ∧ ¬ 𝑥𝑧) → ∃𝑤𝑧 ¬ 𝑤 = 𝑧)
11 equequ2 2130 . . . . . . 7 (𝑧 = 𝑦 → (𝑤 = 𝑧𝑤 = 𝑦))
1211notbid 310 . . . . . 6 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦))
13 ax7 2120 . . . . . . . 8 (𝑥 = 𝑤 → (𝑥 = 𝑦𝑤 = 𝑦))
1413con3d 150 . . . . . . 7 (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦))
1514spimev 2412 . . . . . 6 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
1612, 15syl6bi 245 . . . . 5 (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
17 ax7 2120 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
1817con3d 150 . . . . . . 7 (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦))
1918spimev 2412 . . . . . 6 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦)
2019a1d 25 . . . . 5 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦))
2116, 20pm2.61i 177 . . . 4 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
2221exlimivv 2031 . . 3 (∃𝑤𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)
236, 10, 22mp2b 10 . 2 𝑥 ¬ 𝑥 = 𝑦
24 exnal 1925 . 2 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
2523, 24mpbi 222 1 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386  wal 1654  wex 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-12 2220  ax-13 2389  ax-nul 5013  ax-pow 5065
This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1660  df-ex 1879  df-nf 1883
This theorem is referenced by:  dtrucor  5071  dvdemo1  5073  nfnid  5075  axc16b  5088  eunex  5089  eunexOLD  5090  brprcneu  6425  zfcndpow  9753
  Copyright terms: Public domain W3C validator