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

Theorem exmidexmid 3998
Description: EXMID implies that an arbitrary proposition is decidable. That is, EXMID captures the usual meaning of excluded middle when stated in terms of propositions.

To get other propositional statements which are equivalent to excluded middle, combine this with notnotrdc 787, peircedc 856, or condc 785.

(Contributed by Jim Kingdon, 18-Jun-2022.)

Assertion
Ref Expression
exmidexmid  |-  (EXMID  -> DECID  ph )

Proof of Theorem exmidexmid
Dummy variables  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 3092 . . 3  |-  { z  e.  { (/) }  |  ph }  C_  { (/) }
2 df-exmid 3997 . . . 4  |-  (EXMID  <->  A. x
( x  C_  { (/) }  -> DECID  (/) 
e.  x ) )
3 p0ex 3990 . . . . . 6  |-  { (/) }  e.  _V
43rabex 3951 . . . . 5  |-  { z  e.  { (/) }  |  ph }  e.  _V
5 sseq1 3033 . . . . . 6  |-  ( x  =  { z  e. 
{ (/) }  |  ph }  ->  ( x  C_  {
(/) }  <->  { z  e.  { (/)
}  |  ph }  C_ 
{ (/) } ) )
6 eleq2 2148 . . . . . . 7  |-  ( x  =  { z  e. 
{ (/) }  |  ph }  ->  ( (/)  e.  x  <->  (/)  e.  { z  e.  { (/)
}  |  ph }
) )
76dcbid 784 . . . . . 6  |-  ( x  =  { z  e. 
{ (/) }  |  ph }  ->  (DECID  (/)  e.  x  <-> DECID  (/)  e.  { z  e.  { (/) }  |  ph } ) )
85, 7imbi12d 232 . . . . 5  |-  ( x  =  { z  e. 
{ (/) }  |  ph }  ->  ( ( x 
C_  { (/) }  -> DECID  (/)  e.  x
)  <->  ( { z  e.  { (/) }  |  ph }  C_  { (/) }  -> DECID  (/)  e.  {
z  e.  { (/) }  |  ph } ) ) )
94, 8spcv 2704 . . . 4  |-  ( A. x ( x  C_  {
(/) }  -> DECID  (/)  e.  x )  ->  ( { z  e.  { (/) }  |  ph }  C_  { (/) }  -> DECID  (/)  e.  {
z  e.  { (/) }  |  ph } ) )
102, 9sylbi 119 . . 3  |-  (EXMID  ->  ( { z  e.  { (/)
}  |  ph }  C_ 
{ (/) }  -> DECID  (/)  e.  { z  e.  { (/) }  |  ph } ) )
111, 10mpi 15 . 2  |-  (EXMID  -> DECID  (/)  e.  { z  e.  { (/) }  |  ph } )
12 0ex 3934 . . . . 5  |-  (/)  e.  _V
1312snid 3452 . . . 4  |-  (/)  e.  { (/)
}
14 biidd 170 . . . . 5  |-  ( z  =  (/)  ->  ( ph  <->  ph ) )
1514elrab 2761 . . . 4  |-  ( (/)  e.  { z  e.  { (/)
}  |  ph }  <->  (
(/)  e.  { (/) }  /\  ph ) )
1613, 15mpbiran 884 . . 3  |-  ( (/)  e.  { z  e.  { (/)
}  |  ph }  <->  ph )
1716dcbii 783 . 2  |-  (DECID  (/)  e.  {
z  e.  { (/) }  |  ph }  <-> DECID  ph )
1811, 17sylib 120 1  |-  (EXMID  -> DECID  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4  DECID wdc 778   A.wal 1285    = wceq 1287    e. wcel 1436   {crab 2359    C_ wss 2986   (/)c0 3272   {csn 3425  EXMIDwem 3996
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925  ax-nul 3933  ax-pow 3977
This theorem depends on definitions:  df-bi 115  df-dc 779  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rab 2364  df-v 2616  df-dif 2988  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-exmid 3997
This theorem is referenced by:  exmid0el  4000  exmidel  4001  exmidundif  4002  sbthlemi3  6589  sbthlemi5  6591  sbthlemi6  6592  exmidomniim  6718  exmidfodomrlemim  6748
  Copyright terms: Public domain W3C validator