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

Theorem dtru 4217
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 1670.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2277 or ax-sep 4157. See dtruALT 4223 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

Proof of Theorem dtru
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 el 4208 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4165 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 sp 1728 . . . . . . 7  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
43eximi 1566 . . . . . 6  |-  ( E. z A. x  -.  x  e.  z  ->  E. z  -.  x  e.  z )
52, 4ax-mp 8 . . . . 5  |-  E. z  -.  x  e.  z
6 eeanv 1866 . . . . 5  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
71, 5, 6mpbir2an 886 . . . 4  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
8 ax-14 1700 . . . . . . 7  |-  ( w  =  z  ->  (
x  e.  w  ->  x  e.  z )
)
98com12 27 . . . . . 6  |-  ( x  e.  w  ->  (
w  =  z  ->  x  e.  z )
)
109con3and 428 . . . . 5  |-  ( ( x  e.  w  /\  -.  x  e.  z
)  ->  -.  w  =  z )
11102eximi 1567 . . . 4  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  ->  E. w E. z  -.  w  =  z )
127, 11ax-mp 8 . . 3  |-  E. w E. z  -.  w  =  z
13 equequ2 1669 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1413notbid 285 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
15 ax-8 1661 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1615con3d 125 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1716spimev 1952 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1814, 17syl6bi 219 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
19 ax-8 1661 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
2019con3d 125 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2120spimev 1952 . . . . . 6  |-  ( -.  z  =  y  ->  E. x  -.  x  =  y )
2221a1d 22 . . . . 5  |-  ( -.  z  =  y  -> 
( -.  w  =  z  ->  E. x  -.  x  =  y
) )
2318, 22pm2.61i 156 . . . 4  |-  ( -.  w  =  z  ->  E. x  -.  x  =  y )
2423exlimivv 1625 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2512, 24ax-mp 8 . 2  |-  E. x  -.  x  =  y
26 exnal 1564 . 2  |-  ( E. x  -.  x  =  y  <->  -.  A. x  x  =  y )
2725, 26mpbi 199 1  |-  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696
This theorem is referenced by:  ax16b  4218  eunex  4219  nfnid  4220  dtrucor  4224  dvdemo1  4226  brprcneu  5534  zfcndpow  8254
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-nul 4165  ax-pow 4204
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator