ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  regexmid Unicode version

Theorem regexmid 4280
Description: The axiom of foundation implies excluded middle.

By foundation (or regularity), we mean the principle that every inhabited set has an element which is minimal (when arranged by  e.). The statement of foundation here is taken from Metamath Proof Explorer's ax-reg, and is identical (modulo one unnecessary quantifier) to the statement of foundation in Theorem "Foundation implies instances of EM" of [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

For this reason, IZF does not adopt foundation as an axiom and instead replaces it with ax-setind 4282. (Contributed by Jim Kingdon, 3-Sep-2019.)

Hypothesis
Ref Expression
regexmid.1  |-  ( E. y  y  e.  x  ->  E. y ( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x ) ) )
Assertion
Ref Expression
regexmid  |-  ( ph  \/  -.  ph )
Distinct variable group:    ph, x, y, z

Proof of Theorem regexmid
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 eqid 2082 . . 3  |-  { w  e.  { (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  =  { w  e.  { (/) ,  { (/) } }  | 
( w  =  { (/)
}  \/  ( w  =  (/)  /\  ph )
) }
21regexmidlemm 4277 . 2  |-  E. y 
y  e.  { w  e.  { (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }
3 pp0ex 3962 . . . 4  |-  { (/) ,  { (/) } }  e.  _V
43rabex 3924 . . 3  |-  { w  e.  { (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  e.  _V
5 eleq2 2143 . . . . 5  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( y  e.  x  <->  y  e.  { w  e.  { (/) ,  { (/) } }  | 
( w  =  { (/)
}  \/  ( w  =  (/)  /\  ph )
) } ) )
65exbidv 1747 . . . 4  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( E. y  y  e.  x  <->  E. y  y  e. 
{ w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) )
7 eleq2 2143 . . . . . . . . 9  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( z  e.  x  <->  z  e.  { w  e.  { (/) ,  { (/) } }  | 
( w  =  { (/)
}  \/  ( w  =  (/)  /\  ph )
) } ) )
87notbid 625 . . . . . . . 8  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( -.  z  e.  x  <->  -.  z  e.  { w  e.  { (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) } ) )
98imbi2d 228 . . . . . . 7  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( ( z  e.  y  ->  -.  z  e.  x )  <->  ( z  e.  y  ->  -.  z  e.  { w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) ) )
109albidv 1746 . . . . . 6  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( A. z ( z  e.  y  ->  -.  z  e.  x )  <->  A. z ( z  e.  y  ->  -.  z  e.  { w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) ) )
115, 10anbi12d 457 . . . . 5  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( ( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x )
)  <->  ( y  e. 
{ w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) }  /\  A. z ( z  e.  y  ->  -.  z  e.  { w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) ) ) )
1211exbidv 1747 . . . 4  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( E. y ( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x ) )  <->  E. y
( y  e.  {
w  e.  { (/) ,  { (/) } }  | 
( w  =  { (/)
}  \/  ( w  =  (/)  /\  ph )
) }  /\  A. z ( z  e.  y  ->  -.  z  e.  { w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) ) ) )
136, 12imbi12d 232 . . 3  |-  ( x  =  { w  e. 
{ (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  ( ( E. y  y  e.  x  ->  E. y
( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x )
) )  <->  ( E. y  y  e.  { w  e.  { (/) ,  { (/) } }  |  ( w  =  { (/) }  \/  ( w  =  (/)  /\  ph ) ) }  ->  E. y ( y  e. 
{ w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) }  /\  A. z ( z  e.  y  ->  -.  z  e.  { w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) ) ) ) )
14 regexmid.1 . . 3  |-  ( E. y  y  e.  x  ->  E. y ( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x ) ) )
154, 13, 14vtocl 2654 . 2  |-  ( E. y  y  e.  {
w  e.  { (/) ,  { (/) } }  | 
( w  =  { (/)
}  \/  ( w  =  (/)  /\  ph )
) }  ->  E. y
( y  e.  {
w  e.  { (/) ,  { (/) } }  | 
( w  =  { (/)
}  \/  ( w  =  (/)  /\  ph )
) }  /\  A. z ( z  e.  y  ->  -.  z  e.  { w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) ) )
161regexmidlem1 4278 . 2  |-  ( E. y ( y  e. 
{ w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) }  /\  A. z ( z  e.  y  ->  -.  z  e.  { w  e.  { (/)
,  { (/) } }  |  ( w  =  { (/) }  \/  (
w  =  (/)  /\  ph ) ) } ) )  ->  ( ph  \/  -.  ph ) )
172, 15, 16mp2b 8 1  |-  ( ph  \/  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    \/ wo 662   A.wal 1283    = wceq 1285   E.wex 1422    e. wcel 1434   {crab 2353   (/)c0 3252   {csn 3400   {cpr 3401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3898  ax-nul 3906  ax-pow 3950
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rab 2358  df-v 2604  df-dif 2976  df-un 2978  df-in 2980  df-ss 2987  df-nul 3253  df-pw 3386  df-sn 3406  df-pr 3407
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator