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

Theorem dtru 4201
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  x and  y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 1651.

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

The proof makes use of dummy variables  z and  w which do not appear in the final theorem. They must be distinct from each other and from  x and  y. In other words, if we were to substitute  x for  z throughout the proof, the proof would fail. Although this requirement is made explicitly in the set.mm source file, it is implicit on the web page (i.e. doesn't appear in the "Distinct variable group"). (Contributed by NM, 7-Nov-2006.)

Assertion
Ref Expression
dtru  |-  -.  A. x  x  =  y
Distinct variable group:    x, y
Dummy variables  w  z are mutually distinct and distinct from all other variables.

Proof of Theorem dtru
StepHypRef Expression
1 el 4192 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4151 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 sp 1717 . . . . . . 7  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
43eximi 1564 . . . . . 6  |-  ( E. z A. x  -.  x  e.  z  ->  E. z  -.  x  e.  z )
52, 4ax-mp 10 . . . . 5  |-  E. z  -.  x  e.  z
6 eeanv 1856 . . . . 5  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
71, 5, 6mpbir2an 888 . . . 4  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
8 ax-14 1689 . . . . . . 7  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
98com12 29 . . . . . 6  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
109con3and 430 . . . . 5  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
11102eximi 1565 . . . 4  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  ->  E. w E. z  -.  w  =  z )
127, 11ax-mp 10 . . 3  |-  E. w E. z  -.  w  =  z
13 equequ2 1650 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1413notbid 287 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
15 ax-8 1645 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1615con3d 127 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1716spimev 1945 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1814, 17syl6bi 221 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
19 ax-8 1645 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
2019con3d 127 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2120spimev 1945 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2221a1d 24 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2318, 22pm2.61i 158 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2423exlimivv 1668 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2512, 24ax-mp 10 . 2  |-  E. x  -.  x  =  y
26 exnal 1562 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2725, 26mpbi 201 1  |-  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    /\ wa 360   A.wal 1528   E.wex 1529    = wceq 1624    e. wcel 1685
This theorem is referenced by:  ax16b  4202  eunex  4203  nfnid  4204  dtrucor  4208  dvdemo1  4210  zfcndpow  8234
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-nul 4151  ax-pow 4188
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator