Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  exmid1stab Unicode version

Theorem exmid1stab 13184
Description: If any proposition is stable, excluded middle follows. We are thinking of  x as a proposition and  x  =  { (/)
} as "x is true". (Contributed by Jim Kingdon, 28-Nov-2023.)
Hypothesis
Ref Expression
exmid1stab.x  |-  ( (
ph  /\  x  C_  { (/) } )  -> STAB  x  =  { (/)
} )
Assertion
Ref Expression
exmid1stab  |-  ( ph  -> EXMID )
Distinct variable group:    ph, x

Proof of Theorem exmid1stab
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 0ex 4050 . . . . . . . . 9  |-  (/)  e.  _V
21snid 3551 . . . . . . . 8  |-  (/)  e.  { (/)
}
3 nnexmid 835 . . . . . . . . . . 11  |-  -.  -.  ( y  =  { (/)
}  \/  -.  y  =  { (/) } )
4 uneq1 3218 . . . . . . . . . . . . . . 15  |-  ( y  =  { (/) }  ->  ( y  u.  ( {
(/) }  \  y
) )  =  ( { (/) }  u.  ( { (/) }  \  y
) ) )
5 undifabs 3434 . . . . . . . . . . . . . . 15  |-  ( {
(/) }  u.  ( { (/) }  \  y
) )  =  { (/)
}
64, 5syl6eq 2186 . . . . . . . . . . . . . 14  |-  ( y  =  { (/) }  ->  ( y  u.  ( {
(/) }  \  y
) )  =  { (/)
} )
76a1i 9 . . . . . . . . . . . . 13  |-  ( y 
C_  { (/) }  ->  ( y  =  { (/) }  ->  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } ) )
8 df-ne 2307 . . . . . . . . . . . . . . . . 17  |-  ( y  =/=  { (/) }  <->  -.  y  =  { (/) } )
9 pwntru 4117 . . . . . . . . . . . . . . . . 17  |-  ( ( y  C_  { (/) }  /\  y  =/=  { (/) } )  ->  y  =  (/) )
108, 9sylan2br 286 . . . . . . . . . . . . . . . 16  |-  ( ( y  C_  { (/) }  /\  -.  y  =  { (/)
} )  ->  y  =  (/) )
1110difeq2d 3189 . . . . . . . . . . . . . . . . 17  |-  ( ( y  C_  { (/) }  /\  -.  y  =  { (/)
} )  ->  ( { (/) }  \  y
)  =  ( {
(/) }  \  (/) ) )
12 dif0 3428 . . . . . . . . . . . . . . . . 17  |-  ( {
(/) }  \  (/) )  =  { (/) }
1311, 12syl6eq 2186 . . . . . . . . . . . . . . . 16  |-  ( ( y  C_  { (/) }  /\  -.  y  =  { (/)
} )  ->  ( { (/) }  \  y
)  =  { (/) } )
1410, 13uneq12d 3226 . . . . . . . . . . . . . . 15  |-  ( ( y  C_  { (/) }  /\  -.  y  =  { (/)
} )  ->  (
y  u.  ( {
(/) }  \  y
) )  =  (
(/)  u.  { (/) } ) )
15 uncom 3215 . . . . . . . . . . . . . . . 16  |-  ( (/)  u. 
{ (/) } )  =  ( { (/) }  u.  (/) )
16 un0 3391 . . . . . . . . . . . . . . . 16  |-  ( {
(/) }  u.  (/) )  =  { (/) }
1715, 16eqtri 2158 . . . . . . . . . . . . . . 15  |-  ( (/)  u. 
{ (/) } )  =  { (/) }
1814, 17syl6eq 2186 . . . . . . . . . . . . . 14  |-  ( ( y  C_  { (/) }  /\  -.  y  =  { (/)
} )  ->  (
y  u.  ( {
(/) }  \  y
) )  =  { (/)
} )
1918ex 114 . . . . . . . . . . . . 13  |-  ( y 
C_  { (/) }  ->  ( -.  y  =  { (/)
}  ->  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } ) )
207, 19jaod 706 . . . . . . . . . . . 12  |-  ( y 
C_  { (/) }  ->  ( ( y  =  { (/)
}  \/  -.  y  =  { (/) } )  -> 
( y  u.  ( { (/) }  \  y
) )  =  { (/)
} ) )
2120con3d 620 . . . . . . . . . . 11  |-  ( y 
C_  { (/) }  ->  ( -.  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) }  ->  -.  ( y  =  { (/)
}  \/  -.  y  =  { (/) } ) ) )
223, 21mtoi 653 . . . . . . . . . 10  |-  ( y 
C_  { (/) }  ->  -. 
-.  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } )
2322adantl 275 . . . . . . . . 9  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  -.  -.  ( y  u.  ( { (/) }  \  y
) )  =  { (/)
} )
24 difss 3197 . . . . . . . . . . . . 13  |-  ( {
(/) }  \  y
)  C_  { (/) }
25 unss 3245 . . . . . . . . . . . . . 14  |-  ( ( y  C_  { (/) }  /\  ( { (/) }  \  y
)  C_  { (/) } )  <-> 
( y  u.  ( { (/) }  \  y
) )  C_  { (/) } )
2625biimpi 119 . . . . . . . . . . . . 13  |-  ( ( y  C_  { (/) }  /\  ( { (/) }  \  y
)  C_  { (/) } )  ->  ( y  u.  ( { (/) }  \ 
y ) )  C_  {
(/) } )
2724, 26mpan2 421 . . . . . . . . . . . 12  |-  ( y 
C_  { (/) }  ->  ( y  u.  ( {
(/) }  \  y
) )  C_  { (/) } )
2827adantl 275 . . . . . . . . . . 11  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  (
y  u.  ( {
(/) }  \  y
) )  C_  { (/) } )
29 exmid1stab.x . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  C_  { (/) } )  -> STAB  x  =  { (/)
} )
3029ex 114 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  C_  { (/) }  -> STAB 
x  =  { (/) } ) )
3130alrimiv 1846 . . . . . . . . . . . 12  |-  ( ph  ->  A. x ( x 
C_  { (/) }  -> STAB  x  =  { (/) } ) )
32 p0ex 4107 . . . . . . . . . . . . . 14  |-  { (/) }  e.  _V
3332ssex 4060 . . . . . . . . . . . . 13  |-  ( ( y  u.  ( {
(/) }  \  y
) )  C_  { (/) }  ->  ( y  u.  ( { (/) }  \ 
y ) )  e. 
_V )
34 sseq1 3115 . . . . . . . . . . . . . . 15  |-  ( x  =  ( y  u.  ( { (/) }  \ 
y ) )  -> 
( x  C_  { (/) }  <-> 
( y  u.  ( { (/) }  \  y
) )  C_  { (/) } ) )
35 eqeq1 2144 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( y  u.  ( { (/) }  \ 
y ) )  -> 
( x  =  { (/)
}  <->  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } ) )
3635stbid 817 . . . . . . . . . . . . . . 15  |-  ( x  =  ( y  u.  ( { (/) }  \ 
y ) )  -> 
(STAB  x  =  { (/) }  <-> STAB  (
y  u.  ( {
(/) }  \  y
) )  =  { (/)
} ) )
3734, 36imbi12d 233 . . . . . . . . . . . . . 14  |-  ( x  =  ( y  u.  ( { (/) }  \ 
y ) )  -> 
( ( x  C_  {
(/) }  -> STAB  x  =  { (/)
} )  <->  ( (
y  u.  ( {
(/) }  \  y
) )  C_  { (/) }  -> STAB  ( y  u.  ( { (/) }  \  y
) )  =  { (/)
} ) ) )
3837spcgv 2768 . . . . . . . . . . . . 13  |-  ( ( y  u.  ( {
(/) }  \  y
) )  e.  _V  ->  ( A. x ( x  C_  { (/) }  -> STAB  x  =  { (/) } )  -> 
( ( y  u.  ( { (/) }  \ 
y ) )  C_  {
(/) }  -> STAB  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } ) ) )
3927, 33, 383syl 17 . . . . . . . . . . . 12  |-  ( y 
C_  { (/) }  ->  ( A. x ( x 
C_  { (/) }  -> STAB  x  =  { (/) } )  -> 
( ( y  u.  ( { (/) }  \ 
y ) )  C_  {
(/) }  -> STAB  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } ) ) )
4031, 39mpan9 279 . . . . . . . . . . 11  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  (
( y  u.  ( { (/) }  \  y
) )  C_  { (/) }  -> STAB  ( y  u.  ( { (/) }  \  y
) )  =  { (/)
} ) )
4128, 40mpd 13 . . . . . . . . . 10  |-  ( (
ph  /\  y  C_  {
(/) } )  -> STAB  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } )
42 df-stab 816 . . . . . . . . . 10  |-  (STAB  ( y  u.  ( { (/) } 
\  y ) )  =  { (/) }  <->  ( -.  -.  ( y  u.  ( { (/) }  \  y
) )  =  { (/)
}  ->  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) } ) )
4341, 42sylib 121 . . . . . . . . 9  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  ( -.  -.  ( y  u.  ( { (/) }  \ 
y ) )  =  { (/) }  ->  (
y  u.  ( {
(/) }  \  y
) )  =  { (/)
} ) )
4423, 43mpd 13 . . . . . . . 8  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  (
y  u.  ( {
(/) }  \  y
) )  =  { (/)
} )
452, 44eleqtrrid 2227 . . . . . . 7  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  (/)  e.  ( y  u.  ( {
(/) }  \  y
) ) )
46 elun 3212 . . . . . . 7  |-  ( (/)  e.  ( y  u.  ( { (/) }  \  y
) )  <->  ( (/)  e.  y  \/  (/)  e.  ( {
(/) }  \  y
) ) )
4745, 46sylib 121 . . . . . 6  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  ( (/) 
e.  y  \/  (/)  e.  ( { (/) }  \  y
) ) )
48 eldifn 3194 . . . . . . 7  |-  ( (/)  e.  ( { (/) }  \ 
y )  ->  -.  (/) 
e.  y )
4948orim2i 750 . . . . . 6  |-  ( (
(/)  e.  y  \/  (/) 
e.  ( { (/) } 
\  y ) )  ->  ( (/)  e.  y  \/  -.  (/)  e.  y ) )
5047, 49syl 14 . . . . 5  |-  ( (
ph  /\  y  C_  {
(/) } )  ->  ( (/) 
e.  y  \/  -.  (/) 
e.  y ) )
51 df-dc 820 . . . . 5  |-  (DECID  (/)  e.  y  <-> 
( (/)  e.  y  \/ 
-.  (/)  e.  y ) )
5250, 51sylibr 133 . . . 4  |-  ( (
ph  /\  y  C_  {
(/) } )  -> DECID  (/)  e.  y )
5352ex 114 . . 3  |-  ( ph  ->  ( y  C_  { (/) }  -> DECID  (/) 
e.  y ) )
5453alrimiv 1846 . 2  |-  ( ph  ->  A. y ( y 
C_  { (/) }  -> DECID  (/)  e.  y ) )
55 df-exmid 4114 . 2  |-  (EXMID  <->  A. y
( y  C_  { (/) }  -> DECID  (/) 
e.  y ) )
5654, 55sylibr 133 1  |-  ( ph  -> EXMID )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    \/ wo 697  STAB wstab 815  DECID wdc 819   A.wal 1329    = wceq 1331    e. wcel 1480    =/= wne 2306   _Vcvv 2681    \ cdif 3063    u. cun 3064    C_ wss 3066   (/)c0 3358   {csn 3522  EXMIDwem 4113
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-nul 4049  ax-pow 4093
This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-rab 2423  df-v 2683  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-pw 3507  df-sn 3528  df-exmid 4114
This theorem is referenced by:  subctctexmid  13185
  Copyright terms: Public domain W3C validator