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

Theorem exmidundif 4190
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 3494 and undifdcss 6898 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 3494 . . . . . . . 8  |-  ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  C_  y
)
21biimpi 119 . . . . . . 7  |-  ( x 
C_  y  ->  (
x  u.  ( y 
\  x ) ) 
C_  y )
32adantl 275 . . . . . 6  |-  ( (EXMID  /\  x  C_  y )  ->  ( x  u.  (
y  \  x )
)  C_  y )
4 elun1 3294 . . . . . . . . . . 11  |-  ( z  e.  x  ->  z  e.  ( x  u.  (
y  \  x )
) )
54adantl 275 . . . . . . . . . 10  |-  ( ( (EXMID 
/\  z  e.  y )  /\  z  e.  x )  ->  z  e.  ( x  u.  (
y  \  x )
) )
6 simplr 525 . . . . . . . . . . . 12  |-  ( ( (EXMID 
/\  z  e.  y )  /\  -.  z  e.  x )  ->  z  e.  y )
7 simpr 109 . . . . . . . . . . . 12  |-  ( ( (EXMID 
/\  z  e.  y )  /\  -.  z  e.  x )  ->  -.  z  e.  x )
86, 7eldifd 3131 . . . . . . . . . . 11  |-  ( ( (EXMID 
/\  z  e.  y )  /\  -.  z  e.  x )  ->  z  e.  ( y  \  x
) )
9 elun2 3295 . . . . . . . . . . 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 4180 . . . . . . . . . . . 12  |-  (EXMID  -> DECID  z  e.  x
)
12 exmiddc 831 . . . . . . . . . . . 12  |-  (DECID  z  e.  x  ->  ( z  e.  x  \/  -.  z  e.  x )
)
1311, 12syl 14 . . . . . . . . . . 11  |-  (EXMID  ->  (
z  e.  x  \/ 
-.  z  e.  x
) )
1413adantr 274 . . . . . . . . . 10  |-  ( (EXMID  /\  z  e.  y )  ->  ( z  e.  x  \/  -.  z  e.  x ) )
155, 10, 14mpjaodan 793 . . . . . . . . 9  |-  ( (EXMID  /\  z  e.  y )  ->  z  e.  ( x  u.  ( y 
\  x ) ) )
1615ex 114 . . . . . . . 8  |-  (EXMID  ->  (
z  e.  y  -> 
z  e.  ( x  u.  ( y  \  x ) ) ) )
1716ssrdv 3153 . . . . . . 7  |-  (EXMID  ->  y  C_  ( x  u.  (
y  \  x )
) )
1817adantr 274 . . . . . 6  |-  ( (EXMID  /\  x  C_  y )  ->  y  C_  ( x  u.  ( y  \  x
) ) )
193, 18eqssd 3164 . . . . 5  |-  ( (EXMID  /\  x  C_  y )  ->  ( x  u.  (
y  \  x )
)  =  y )
2019ex 114 . . . 4  |-  (EXMID  ->  (
x  C_  y  ->  ( x  u.  ( y 
\  x ) )  =  y ) )
21 ssun1 3290 . . . . 5  |-  x  C_  ( x  u.  (
y  \  x )
)
22 sseq2 3171 . . . . 5  |-  ( ( x  u.  ( y 
\  x ) )  =  y  ->  (
x  C_  ( x  u.  ( y  \  x
) )  <->  x  C_  y
) )
2321, 22mpbii 147 . . . 4  |-  ( ( x  u.  ( y 
\  x ) )  =  y  ->  x  C_  y )
2420, 23impbid1 141 . . 3  |-  (EXMID  ->  (
x  C_  y  <->  ( x  u.  ( y  \  x
) )  =  y ) )
2524alrimivv 1868 . 2  |-  (EXMID  ->  A. x A. y ( x  C_  y 
<->  ( x  u.  (
y  \  x )
)  =  y ) )
26 vex 2733 . . . . . 6  |-  z  e. 
_V
27 p0ex 4172 . . . . . 6  |-  { (/) }  e.  _V
28 sseq12 3172 . . . . . . . 8  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( x  C_  y 
<->  z  C_  { (/) } ) )
29 simpl 108 . . . . . . . . . 10  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  x  =  z )
30 simpr 109 . . . . . . . . . . 11  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  y  =  { (/)
} )
3130, 29difeq12d 3246 . . . . . . . . . 10  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( y  \  x )  =  ( { (/) }  \  z
) )
3229, 31uneq12d 3282 . . . . . . . . 9  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( x  u.  ( y  \  x
) )  =  ( z  u.  ( {
(/) }  \  z
) ) )
3332, 30eqeq12d 2185 . . . . . . . 8  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( ( x  u.  ( y  \  x ) )  =  y  <->  ( z  u.  ( { (/) }  \ 
z ) )  =  { (/) } ) )
3428, 33bibi12d 234 . . . . . . 7  |-  ( ( x  =  z  /\  y  =  { (/) } )  ->  ( ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  <->  ( z  C_  {
(/) }  <->  ( z  u.  ( { (/) }  \ 
z ) )  =  { (/) } ) ) )
3534spc2gv 2821 . . . . . 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 424 . . . . 5  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  ->  ( z  C_ 
{ (/) }  <->  ( z  u.  ( { (/) }  \ 
z ) )  =  { (/) } ) )
37 0ex 4114 . . . . . . . 8  |-  (/)  e.  _V
3837snid 3612 . . . . . . 7  |-  (/)  e.  { (/)
}
39 eleq2 2234 . . . . . . 7  |-  ( ( z  u.  ( {
(/) }  \  z
) )  =  { (/)
}  ->  ( (/)  e.  ( z  u.  ( {
(/) }  \  z
) )  <->  (/)  e.  { (/)
} ) )
4038, 39mpbiri 167 . . . . . 6  |-  ( ( z  u.  ( {
(/) }  \  z
) )  =  { (/)
}  ->  (/)  e.  ( z  u.  ( {
(/) }  \  z
) ) )
41 eldifn 3250 . . . . . . . 8  |-  ( (/)  e.  ( { (/) }  \ 
z )  ->  -.  (/) 
e.  z )
4241orim2i 756 . . . . . . 7  |-  ( (
(/)  e.  z  \/  (/) 
e.  ( { (/) } 
\  z ) )  ->  ( (/)  e.  z  \/  -.  (/)  e.  z ) )
43 elun 3268 . . . . . . 7  |-  ( (/)  e.  ( z  u.  ( { (/) }  \  z
) )  <->  ( (/)  e.  z  \/  (/)  e.  ( {
(/) }  \  z
) ) )
44 df-dc 830 . . . . . . 7  |-  (DECID  (/)  e.  z  <-> 
( (/)  e.  z  \/ 
-.  (/)  e.  z ) )
4542, 43, 443imtr4i 200 . . . . . 6  |-  ( (/)  e.  ( z  u.  ( { (/) }  \  z
) )  -> DECID  (/)  e.  z )
4640, 45syl 14 . . . . 5  |-  ( ( z  u.  ( {
(/) }  \  z
) )  =  { (/)
}  -> DECID  (/)  e.  z )
4736, 46syl6bi 162 . . . 4  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  ->  ( z  C_ 
{ (/) }  -> DECID  (/)  e.  z ) )
4847alrimiv 1867 . . 3  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  ->  A. z
( z  C_  { (/) }  -> DECID  (/) 
e.  z ) )
49 df-exmid 4179 . . 3  |-  (EXMID  <->  A. z
( z  C_  { (/) }  -> DECID  (/) 
e.  z ) )
5048, 49sylibr 133 . 2  |-  ( A. x A. y ( x 
C_  y  <->  ( x  u.  ( y  \  x
) )  =  y )  -> EXMID )
5125, 50impbii 125 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 103    <-> wb 104    \/ wo 703  DECID wdc 829   A.wal 1346    = wceq 1348    e. wcel 2141   _Vcvv 2730    \ cdif 3118    u. cun 3119    C_ wss 3121   (/)c0 3414   {csn 3581  EXMIDwem 4178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-nul 4113  ax-pow 4158
This theorem depends on definitions:  df-bi 116  df-dc 830  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rab 2457  df-v 2732  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-exmid 4179
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator