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

Theorem exmidundif 4026
Description: Excluded middle is equivalent to every subset having a complement. That is, the union of a subset and its relative complement being the whole set. Although special cases such as undifss 3359 and undifdcss 6613 are provable, the full statement is equivalent to excluded middle as shown here. (Contributed by Jim Kingdon, 18-Jun-2022.)
Assertion
Ref Expression
exmidundif  |-  (EXMID  <->  A. x A. y ( x  C_  y 
<->  ( x  u.  (
y  \  x )
)  =  y ) )
Distinct variable group:    x, y

Proof of Theorem exmidundif
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 undifss 3359 . . . . . . . 8  |-  ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  C_  y
)
21biimpi 118 . . . . . . 7  |-  ( x 
C_  y  ->  (
x  u.  ( y 
\  x ) ) 
C_  y )
32adantl 271 . . . . . 6  |-  ( (EXMID  /\  x  C_  y )  ->  ( x  u.  (
y  \  x )
)  C_  y )
4 elun1 3165 . . . . . . . . . . 11  |-  ( z  e.  x  ->  z  e.  ( x  u.  (
y  \  x )
) )
54adantl 271 . . . . . . . . . 10  |-  ( ( (EXMID 
/\  z  e.  y )  /\  z  e.  x )  ->  z  e.  ( x  u.  (
y  \  x )
) )
6 simplr 497 . . . . . . . . . . . 12  |-  ( ( (EXMID 
/\  z  e.  y )  /\  -.  z  e.  x )  ->  z  e.  y )
7 simpr 108 . . . . . . . . . . . 12  |-  ( ( (EXMID 
/\  z  e.  y )  /\  -.  z  e.  x )  ->  -.  z  e.  x )
86, 7eldifd 3007 . . . . . . . . . . 11  |-  ( ( (EXMID 
/\  z  e.  y )  /\  -.  z  e.  x )  ->  z  e.  ( y  \  x
) )
9 elun2 3166 . . . . . . . . . . 11  |-  ( z  e.  ( y  \  x )  ->  z  e.  ( x  u.  (
y  \  x )
) )
108, 9syl 14 . . . . . . . . . 10  |-  ( ( (EXMID 
/\  z  e.  y )  /\  -.  z  e.  x )  ->  z  e.  ( x  u.  (
y  \  x )
) )
11 exmidexmid 4022 . . . . . . . . . . . 12  |-  (EXMID  -> DECID  z  e.  x
)
12 exmiddc 782 . . . . . . . . . . . 12  |-  (DECID  z  e.  x  ->  ( z  e.  x  \/  -.  z  e.  x )
)
1311, 12syl 14 . . . . . . . . . . 11  |-  (EXMID  ->  (
z  e.  x  \/ 
-.  z  e.  x
) )
1413adantr 270 . . . . . . . . . 10  |-  ( (EXMID  /\  z  e.  y )  ->  ( z  e.  x  \/  -.  z  e.  x ) )
155, 10, 14mpjaodan 747 . . . . . . . . 9  |-  ( (EXMID  /\  z  e.  y )  ->  z  e.  ( x  u.  ( y 
\  x ) ) )
1615ex 113 . . . . . . . 8  |-  (EXMID  ->  (
z  e.  y  -> 
z  e.  ( x  u.  ( y  \  x ) ) ) )
1716ssrdv 3029 . . . . . . 7  |-  (EXMID  ->  y  C_  ( x  u.  (
y  \  x )
) )
1817adantr 270 . . . . . 6  |-  ( (EXMID  /\  x  C_  y )  ->  y  C_  ( x  u.  ( y  \  x
) ) )
193, 18eqssd 3040 . . . . 5  |-  ( (EXMID  /\  x  C_  y )  ->  ( x  u.  (
y  \  x )
)  =  y )
2019ex 113 . . . 4  |-  (EXMID  ->  (
x  C_  y  ->  ( x  u.  ( y 
\  x ) )  =  y ) )
21 ssun1 3161 . . . . 5  |-  x  C_  ( x  u.  (
y  \  x )
)
22 sseq2 3046 . . . . 5  |-  ( ( x  u.  ( y 
\  x ) )  =  y  ->  (
x  C_  ( x  u.  ( y  \  x
) )  <->  x  C_  y
) )
2321, 22mpbii 146 . . . 4  |-  ( ( x  u.  ( y 
\  x ) )  =  y  ->  x  C_  y )
2420, 23impbid1 140 . . 3  |-  (EXMID  ->  (
x  C_  y  <->  ( x  u.  ( y  \  x
) )  =  y ) )
2524alrimivv 1803 . 2  |-  (EXMID  ->  A. x A. y ( x  C_  y 
<->  ( x  u.  (
y  \  x )
)  =  y ) )
26 vex 2622 . . . . . 6  |-  z  e. 
_V
27 p0ex 4014 . . . . . 6  |-  { (/) }  e.  _V
28 sseq12 3047 . . . . . . . 8  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( x  C_  y 
<->  z  C_  { (/) } ) )
29 simpl 107 . . . . . . . . . 10  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  x  =  z )
30 simpr 108 . . . . . . . . . . 11  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  y  =  { (/)
} )
3130, 29difeq12d 3117 . . . . . . . . . 10  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( y  \  x )  =  ( { (/) }  \  z
) )
3229, 31uneq12d 3153 . . . . . . . . 9  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( x  u.  ( y  \  x
) )  =  ( z  u.  ( {
(/) }  \  z
) ) )
3332, 30eqeq12d 2102 . . . . . . . 8  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( ( x  u.  ( y  \  x ) )  =  y  <->  ( z  u.  ( { (/) }  \ 
z ) )  =  { (/) } ) )
3428, 33bibi12d 233 . . . . . . 7  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  <->  ( z  C_  {
(/) }  <->  ( z  u.  ( { (/) }  \ 
z ) )  =  { (/) } ) ) )
3534spc2gv 2709 . . . . . 6  |-  ( ( z  e.  _V  /\  {
(/) }  e.  _V )  ->  ( A. x A. y ( x  C_  y 
<->  ( x  u.  (
y  \  x )
)  =  y )  ->  ( z  C_  {
(/) }  <->  ( z  u.  ( { (/) }  \ 
z ) )  =  { (/) } ) ) )
3626, 27, 35mp2an 417 . . . . 5  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  ->  ( z  C_ 
{ (/) }  <->  ( z  u.  ( { (/) }  \ 
z ) )  =  { (/) } ) )
37 0ex 3958 . . . . . . . 8  |-  (/)  e.  _V
3837snid 3470 . . . . . . 7  |-  (/)  e.  { (/)
}
39 eleq2 2151 . . . . . . 7  |-  ( ( z  u.  ( {
(/) }  \  z
) )  =  { (/)
}  ->  ( (/)  e.  ( z  u.  ( {
(/) }  \  z
) )  <->  (/)  e.  { (/)
} ) )
4038, 39mpbiri 166 . . . . . 6  |-  ( ( z  u.  ( {
(/) }  \  z
) )  =  { (/)
}  ->  (/)  e.  ( z  u.  ( {
(/) }  \  z
) ) )
41 eldifn 3121 . . . . . . . 8  |-  ( (/)  e.  ( { (/) }  \ 
z )  ->  -.  (/) 
e.  z )
4241orim2i 713 . . . . . . 7  |-  ( (
(/)  e.  z  \/  (/) 
e.  ( { (/) } 
\  z ) )  ->  ( (/)  e.  z  \/  -.  (/)  e.  z ) )
43 elun 3139 . . . . . . 7  |-  ( (/)  e.  ( z  u.  ( { (/) }  \  z
) )  <->  ( (/)  e.  z  \/  (/)  e.  ( {
(/) }  \  z
) ) )
44 df-dc 781 . . . . . . 7  |-  (DECID  (/)  e.  z  <-> 
( (/)  e.  z  \/ 
-.  (/)  e.  z ) )
4542, 43, 443imtr4i 199 . . . . . 6  |-  ( (/)  e.  ( z  u.  ( { (/) }  \  z
) )  -> DECID  (/)  e.  z )
4640, 45syl 14 . . . . 5  |-  ( ( z  u.  ( {
(/) }  \  z
) )  =  { (/)
}  -> DECID  (/)  e.  z )
4736, 46syl6bi 161 . . . 4  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  ->  ( z  C_ 
{ (/) }  -> DECID  (/)  e.  z ) )
4847alrimiv 1802 . . 3  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  ->  A. z
( z  C_  { (/) }  -> DECID  (/) 
e.  z ) )
49 df-exmid 4021 . . 3  |-  (EXMID  <->  A. z
( z  C_  { (/) }  -> DECID  (/) 
e.  z ) )
5048, 49sylibr 132 . 2  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  -> EXMID )
5125, 50impbii 124 1  |-  (EXMID  <->  A. x A. y ( x  C_  y 
<->  ( x  u.  (
y  \  x )
)  =  y ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 664  DECID wdc 780   A.wal 1287    = wceq 1289    e. wcel 1438   _Vcvv 2619    \ cdif 2994    u. cun 2995    C_ wss 2997   (/)c0 3284   {csn 3441  EXMIDwem 4020
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 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-nul 3957  ax-pow 4001
This theorem depends on definitions:  df-bi 115  df-dc 781  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rab 2368  df-v 2621  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-exmid 4021
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator