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

Theorem dtru 4159
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 1821.

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2237 or ax-sep 4101. See dtruALT 4165 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
StepHypRef Expression
1 el 4150 . . . . 5  |-  E. w  x  e.  w
2 ax-nul 4109 . . . . . 6  |-  E. z A. x  -.  x  e.  z
3 ax-4 1692 . . . . . . 7  |-  ( A. x  -.  x  e.  z  ->  -.  x  e.  z )
43eximi 1574 . . . . . 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 2058 . . . . 5  |-  ( E. w E. z ( x  e.  w  /\  -.  x  e.  z
)  <->  ( E. w  x  e.  w  /\  E. z  -.  x  e.  z ) )
71, 5, 6mpbir2an 891 . . . 4  |-  E. w E. z ( x  e.  w  /\  -.  x  e.  z )
8 ax-14 1626 . . . . . . 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 1575 . . . 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 1830 . . . . . . 7  |-  ( z  =  y  ->  (
w  =  z  <->  w  =  y ) )
1413notbid 287 . . . . . 6  |-  ( z  =  y  ->  ( -.  w  =  z  <->  -.  w  =  y ) )
15 ax-8 1623 . . . . . . . 8  |-  ( x  =  w  ->  (
x  =  y  ->  w  =  y )
)
1615con3d 127 . . . . . . 7  |-  ( x  =  w  ->  ( -.  w  =  y  ->  -.  x  =  y ) )
1716a4imev 1998 . . . . . 6  |-  ( -.  w  =  y  ->  E. x  -.  x  =  y )
1814, 17syl6bi 221 . . . . 5  |-  ( z  =  y  ->  ( -.  w  =  z  ->  E. x  -.  x  =  y ) )
19 ax-8 1623 . . . . . . . 8  |-  ( x  =  z  ->  (
x  =  y  -> 
z  =  y ) )
2019con3d 127 . . . . . . 7  |-  ( x  =  z  ->  ( -.  z  =  y  ->  -.  x  =  y ) )
2120a4imev 1998 . . . . . 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 2026 . . 3  |-  ( E. w E. z  -.  w  =  z  ->  E. x  -.  x  =  y )
2512, 24ax-mp 10 . 2  |-  E. x  -.  x  =  y
26 exnal 1572 . 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 1532   E.wex 1537    = wceq 1619    e. wcel 1621
This theorem is referenced by:  ax16b  4160  eunex  4161  nfnid  4162  dtrucor  4166  dvdemo1  4168  zfcndpow  8192
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-13 1625  ax-14 1626  ax-17 1628  ax-9 1684  ax-4 1692  ax-nul 4109  ax-pow 4146
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator