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

Theorem exmidsssn 4214
Description: Excluded middle is equivalent to the biconditionalized version of sssnr 3765 for sets. (Contributed by Jim Kingdon, 5-Mar-2023.)
Assertion
Ref Expression
exmidsssn  |-  (EXMID  <->  A. x A. y ( x  C_  { y }  <->  ( x  =  (/)  \/  x  =  { y } ) ) )
Distinct variable group:    x, y

Proof of Theorem exmidsssn
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 0ss 3473 . . . . . . 7  |-  (/)  C_  { y }
2 sseq1 3190 . . . . . . 7  |-  ( x  =  (/)  ->  ( x 
C_  { y }  <->  (/)  C_  { y } ) )
31, 2mpbiri 168 . . . . . 6  |-  ( x  =  (/)  ->  x  C_  { y } )
43adantl 277 . . . . 5  |-  ( (EXMID  /\  x  =  (/) )  ->  x  C_  { y } )
5 simpr 110 . . . . . 6  |-  ( (EXMID  /\  x  =  (/) )  ->  x  =  (/) )
65orcd 734 . . . . 5  |-  ( (EXMID  /\  x  =  (/) )  -> 
( x  =  (/)  \/  x  =  { y } ) )
74, 62thd 175 . . . 4  |-  ( (EXMID  /\  x  =  (/) )  -> 
( x  C_  { y }  <->  ( x  =  (/)  \/  x  =  {
y } ) ) )
8 sssnm 3766 . . . . . 6  |-  ( E. z  z  e.  x  ->  ( x  C_  { y }  <->  x  =  {
y } ) )
9 neq0r 3449 . . . . . . 7  |-  ( E. z  z  e.  x  ->  -.  x  =  (/) )
10 biorf 745 . . . . . . 7  |-  ( -.  x  =  (/)  ->  (
x  =  { y }  <->  ( x  =  (/)  \/  x  =  {
y } ) ) )
119, 10syl 14 . . . . . 6  |-  ( E. z  z  e.  x  ->  ( x  =  {
y }  <->  ( x  =  (/)  \/  x  =  { y } ) ) )
128, 11bitrd 188 . . . . 5  |-  ( E. z  z  e.  x  ->  ( x  C_  { y }  <->  ( x  =  (/)  \/  x  =  {
y } ) ) )
1312adantl 277 . . . 4  |-  ( (EXMID  /\ 
E. z  z  e.  x )  ->  (
x  C_  { y } 
<->  ( x  =  (/)  \/  x  =  { y } ) ) )
14 exmidn0m 4213 . . . . . 6  |-  (EXMID  <->  A. x
( x  =  (/)  \/ 
E. z  z  e.  x ) )
1514biimpi 120 . . . . 5  |-  (EXMID  ->  A. x
( x  =  (/)  \/ 
E. z  z  e.  x ) )
161519.21bi 1568 . . . 4  |-  (EXMID  ->  (
x  =  (/)  \/  E. z  z  e.  x
) )
177, 13, 16mpjaodan 799 . . 3  |-  (EXMID  ->  (
x  C_  { y } 
<->  ( x  =  (/)  \/  x  =  { y } ) ) )
1817alrimivv 1885 . 2  |-  (EXMID  ->  A. x A. y ( x  C_  { y }  <->  ( x  =  (/)  \/  x  =  { y } ) ) )
19 0ex 4142 . . . . . 6  |-  (/)  e.  _V
20 sneq 3615 . . . . . . . 8  |-  ( y  =  (/)  ->  { y }  =  { (/) } )
2120sseq2d 3197 . . . . . . 7  |-  ( y  =  (/)  ->  ( x 
C_  { y }  <-> 
x  C_  { (/) } ) )
2220eqeq2d 2199 . . . . . . . 8  |-  ( y  =  (/)  ->  ( x  =  { y }  <-> 
x  =  { (/) } ) )
2322orbi2d 791 . . . . . . 7  |-  ( y  =  (/)  ->  ( ( x  =  (/)  \/  x  =  { y } )  <-> 
( x  =  (/)  \/  x  =  { (/) } ) ) )
2421, 23bibi12d 235 . . . . . 6  |-  ( y  =  (/)  ->  ( ( x  C_  { y } 
<->  ( x  =  (/)  \/  x  =  { y } ) )  <->  ( x  C_ 
{ (/) }  <->  ( x  =  (/)  \/  x  =  { (/) } ) ) ) )
2519, 24spcv 2843 . . . . 5  |-  ( A. y ( x  C_  { y }  <->  ( x  =  (/)  \/  x  =  { y } ) )  ->  ( x  C_ 
{ (/) }  <->  ( x  =  (/)  \/  x  =  { (/) } ) ) )
2625biimpd 144 . . . 4  |-  ( A. y ( x  C_  { y }  <->  ( x  =  (/)  \/  x  =  { y } ) )  ->  ( x  C_ 
{ (/) }  ->  (
x  =  (/)  \/  x  =  { (/) } ) ) )
2726alimi 1465 . . 3  |-  ( A. x A. y ( x 
C_  { y }  <-> 
( x  =  (/)  \/  x  =  { y } ) )  ->  A. x ( x  C_  {
(/) }  ->  ( x  =  (/)  \/  x  =  { (/) } ) ) )
28 exmid01 4210 . . 3  |-  (EXMID  <->  A. x
( x  C_  { (/) }  ->  ( x  =  (/)  \/  x  =  { (/)
} ) ) )
2927, 28sylibr 134 . 2  |-  ( A. x A. y ( x 
C_  { y }  <-> 
( x  =  (/)  \/  x  =  { y } ) )  -> EXMID )
3018, 29impbii 126 1  |-  (EXMID  <->  A. x A. y ( x  C_  { y }  <->  ( x  =  (/)  \/  x  =  { y } ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709   A.wal 1361    = wceq 1363   E.wex 1502    C_ wss 3141   (/)c0 3434   {csn 3604  EXMIDwem 4206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-nul 4141  ax-pow 4186
This theorem depends on definitions:  df-bi 117  df-dc 836  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-rab 2474  df-v 2751  df-dif 3143  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-exmid 4207
This theorem is referenced by:  exmidsssnc  4215
  Copyright terms: Public domain W3C validator