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

Theorem exmidomni 6719
Description: Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
Assertion
Ref Expression
exmidomni  |-  (EXMID  <->  A. x  x  e. Omni )

Proof of Theorem exmidomni
Dummy variables  u  f  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 exmidomniim 6718 . 2  |-  (EXMID  ->  A. x  x  e. Omni )
2 vex 2617 . . . . . . . . . 10  |-  u  e. 
_V
3 eleq1w 2145 . . . . . . . . . 10  |-  ( x  =  u  ->  (
x  e. Omni  <->  u  e. Omni ) )
42, 3spcv 2704 . . . . . . . . 9  |-  ( A. x  x  e. Omni  ->  u  e. Omni )
5 xpeq1 4418 . . . . . . . . . . . . . 14  |-  ( x  =  u  ->  (
x  X.  { (/) } )  =  ( u  X.  { (/) } ) )
65fveq1d 5258 . . . . . . . . . . . . 13  |-  ( x  =  u  ->  (
( x  X.  { (/)
} ) `  y
)  =  ( ( u  X.  { (/) } ) `  y ) )
76eqeq1d 2093 . . . . . . . . . . . 12  |-  ( x  =  u  ->  (
( ( x  X.  { (/) } ) `  y )  =  (/)  <->  (
( u  X.  { (/)
} ) `  y
)  =  (/) ) )
87rexeqbi1dv 2566 . . . . . . . . . . 11  |-  ( x  =  u  ->  ( E. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  (/)  <->  E. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  (/) ) )
96eqeq1d 2093 . . . . . . . . . . . 12  |-  ( x  =  u  ->  (
( ( x  X.  { (/) } ) `  y )  =  1o  <->  ( ( u  X.  { (/)
} ) `  y
)  =  1o ) )
109raleqbi1dv 2565 . . . . . . . . . . 11  |-  ( x  =  u  ->  ( A. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  1o  <->  A. y  e.  u  ( ( u  X.  { (/)
} ) `  y
)  =  1o ) )
118, 10orbi12d 740 . . . . . . . . . 10  |-  ( x  =  u  ->  (
( E. y  e.  x  ( ( x  X.  { (/) } ) `
 y )  =  (/)  \/  A. y  e.  x  ( ( x  X.  { (/) } ) `
 y )  =  1o )  <->  ( E. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  (/)  \/  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o ) ) )
12 vex 2617 . . . . . . . . . . . . 13  |-  x  e. 
_V
13 isomni 6713 . . . . . . . . . . . . 13  |-  ( x  e.  _V  ->  (
x  e. Omni  <->  A. f ( f : x --> 2o  ->  ( E. y  e.  x  ( f `  y
)  =  (/)  \/  A. y  e.  x  (
f `  y )  =  1o ) ) ) )
1412, 13ax-mp 7 . . . . . . . . . . . 12  |-  ( x  e. Omni 
<-> 
A. f ( f : x --> 2o  ->  ( E. y  e.  x  ( f `  y
)  =  (/)  \/  A. y  e.  x  (
f `  y )  =  1o ) ) )
1514biimpi 118 . . . . . . . . . . 11  |-  ( x  e. Omni  ->  A. f ( f : x --> 2o  ->  ( E. y  e.  x  ( f `  y
)  =  (/)  \/  A. y  e.  x  (
f `  y )  =  1o ) ) )
16 0ex 3934 . . . . . . . . . . . . . 14  |-  (/)  e.  _V
1716prid1 3525 . . . . . . . . . . . . 13  |-  (/)  e.  { (/)
,  1o }
18 df2o3 6130 . . . . . . . . . . . . 13  |-  2o  =  { (/) ,  1o }
1917, 18eleqtrri 2160 . . . . . . . . . . . 12  |-  (/)  e.  2o
2019fconst6 5161 . . . . . . . . . . 11  |-  ( x  X.  { (/) } ) : x --> 2o
21 p0ex 3990 . . . . . . . . . . . . 13  |-  { (/) }  e.  _V
2212, 21xpex 4514 . . . . . . . . . . . 12  |-  ( x  X.  { (/) } )  e.  _V
23 feq1 5101 . . . . . . . . . . . . 13  |-  ( f  =  ( x  X.  { (/) } )  -> 
( f : x --> 2o  <->  ( x  X.  { (/) } ) : x --> 2o ) )
24 fveq1 5255 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( x  X.  { (/) } )  -> 
( f `  y
)  =  ( ( x  X.  { (/) } ) `  y ) )
2524eqeq1d 2093 . . . . . . . . . . . . . . 15  |-  ( f  =  ( x  X.  { (/) } )  -> 
( ( f `  y )  =  (/)  <->  (
( x  X.  { (/)
} ) `  y
)  =  (/) ) )
2625rexbidv 2377 . . . . . . . . . . . . . 14  |-  ( f  =  ( x  X.  { (/) } )  -> 
( E. y  e.  x  ( f `  y )  =  (/)  <->  E. y  e.  x  (
( x  X.  { (/)
} ) `  y
)  =  (/) ) )
2724eqeq1d 2093 . . . . . . . . . . . . . . 15  |-  ( f  =  ( x  X.  { (/) } )  -> 
( ( f `  y )  =  1o  <->  ( ( x  X.  { (/)
} ) `  y
)  =  1o ) )
2827ralbidv 2376 . . . . . . . . . . . . . 14  |-  ( f  =  ( x  X.  { (/) } )  -> 
( A. y  e.  x  ( f `  y )  =  1o  <->  A. y  e.  x  ( ( x  X.  { (/)
} ) `  y
)  =  1o ) )
2926, 28orbi12d 740 . . . . . . . . . . . . 13  |-  ( f  =  ( x  X.  { (/) } )  -> 
( ( E. y  e.  x  ( f `  y )  =  (/)  \/ 
A. y  e.  x  ( f `  y
)  =  1o )  <-> 
( E. y  e.  x  ( ( x  X.  { (/) } ) `
 y )  =  (/)  \/  A. y  e.  x  ( ( x  X.  { (/) } ) `
 y )  =  1o ) ) )
3023, 29imbi12d 232 . . . . . . . . . . . 12  |-  ( f  =  ( x  X.  { (/) } )  -> 
( ( f : x --> 2o  ->  ( E. y  e.  x  ( f `  y
)  =  (/)  \/  A. y  e.  x  (
f `  y )  =  1o ) )  <->  ( (
x  X.  { (/) } ) : x --> 2o  ->  ( E. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  (/)  \/ 
A. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  1o ) ) ) )
3122, 30spcv 2704 . . . . . . . . . . 11  |-  ( A. f ( f : x --> 2o  ->  ( E. y  e.  x  ( f `  y
)  =  (/)  \/  A. y  e.  x  (
f `  y )  =  1o ) )  -> 
( ( x  X.  { (/) } ) : x --> 2o  ->  ( E. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  (/)  \/ 
A. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  1o ) ) )
3215, 20, 31mpisyl 1378 . . . . . . . . . 10  |-  ( x  e. Omni  ->  ( E. y  e.  x  ( (
x  X.  { (/) } ) `  y )  =  (/)  \/  A. y  e.  x  ( (
x  X.  { (/) } ) `  y )  =  1o ) )
3311, 32vtoclga 2677 . . . . . . . . 9  |-  ( u  e. Omni  ->  ( E. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  (/)  \/  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o ) )
344, 33syl 14 . . . . . . . 8  |-  ( A. x  x  e. Omni  ->  ( E. y  e.  u  ( ( u  X.  { (/) } ) `  y )  =  (/)  \/ 
A. y  e.  u  ( ( u  X.  { (/) } ) `  y )  =  1o ) )
3534adantr 270 . . . . . . 7  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( E. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  (/)  \/  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o ) )
36 simplr 497 . . . . . . . . . 10  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  E. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  (/) )  ->  u  C_ 
{ (/) } )
37 rexm 3365 . . . . . . . . . . . 12  |-  ( E. y  e.  u  ( ( u  X.  { (/)
} ) `  y
)  =  (/)  ->  E. y 
y  e.  u )
38 sssnm 3575 . . . . . . . . . . . 12  |-  ( E. y  y  e.  u  ->  ( u  C_  { (/) }  <-> 
u  =  { (/) } ) )
3937, 38syl 14 . . . . . . . . . . 11  |-  ( E. y  e.  u  ( ( u  X.  { (/)
} ) `  y
)  =  (/)  ->  (
u  C_  { (/) }  <->  u  =  { (/) } ) )
4039adantl 271 . . . . . . . . . 10  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  E. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  (/) )  ->  (
u  C_  { (/) }  <->  u  =  { (/) } ) )
4136, 40mpbid 145 . . . . . . . . 9  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  E. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  (/) )  ->  u  =  { (/) } )
4241ex 113 . . . . . . . 8  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( E. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  (/)  ->  u  =  { (/) } ) )
43 nfv 1464 . . . . . . . . . . . 12  |-  F/ y ( A. x  x  e. Omni  /\  u  C_  { (/) } )
44 nfra1 2405 . . . . . . . . . . . 12  |-  F/ y A. y  e.  u  ( ( u  X.  { (/) } ) `  y )  =  1o
4543, 44nfan 1500 . . . . . . . . . . 11  |-  F/ y ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )
46 nfcv 2225 . . . . . . . . . . 11  |-  F/_ y
u
47 nfcv 2225 . . . . . . . . . . 11  |-  F/_ y (/)
48 1n0 6132 . . . . . . . . . . . . . 14  |-  1o  =/=  (/)
4948neii 2253 . . . . . . . . . . . . 13  |-  -.  1o  =  (/)
50 simpr 108 . . . . . . . . . . . . . . . 16  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  ->  A. y  e.  u  ( ( u  X.  { (/) } ) `  y )  =  1o )
5150r19.21bi 2457 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )  /\  y  e.  u
)  ->  ( (
u  X.  { (/) } ) `  y )  =  1o )
5216fvconst2 5456 . . . . . . . . . . . . . . . 16  |-  ( y  e.  u  ->  (
( u  X.  { (/)
} ) `  y
)  =  (/) )
5352adantl 271 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )  /\  y  e.  u
)  ->  ( (
u  X.  { (/) } ) `  y )  =  (/) )
5451, 53eqtr3d 2119 . . . . . . . . . . . . . 14  |-  ( ( ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )  /\  y  e.  u
)  ->  1o  =  (/) )
5554ex 113 . . . . . . . . . . . . 13  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  -> 
( y  e.  u  ->  1o  =  (/) ) )
5649, 55mtoi 623 . . . . . . . . . . . 12  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  ->  -.  y  e.  u
)
5756pm2.21d 582 . . . . . . . . . . 11  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  -> 
( y  e.  u  ->  y  e.  (/) ) )
5845, 46, 47, 57ssrd 3017 . . . . . . . . . 10  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  ->  u  C_  (/) )
59 ss0 3308 . . . . . . . . . 10  |-  ( u 
C_  (/)  ->  u  =  (/) )
6058, 59syl 14 . . . . . . . . 9  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  ->  u  =  (/) )
6160ex 113 . . . . . . . 8  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o  ->  u  =  (/) ) )
6242, 61orim12d 733 . . . . . . 7  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( ( E. y  e.  u  ( ( u  X.  { (/) } ) `  y )  =  (/)  \/ 
A. y  e.  u  ( ( u  X.  { (/) } ) `  y )  =  1o )  ->  ( u  =  { (/) }  \/  u  =  (/) ) ) )
6335, 62mpd 13 . . . . . 6  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( u  =  { (/) }  \/  u  =  (/) ) )
6463orcomd 681 . . . . 5  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( u  =  (/)  \/  u  =  { (/) } ) )
6564ex 113 . . . 4  |-  ( A. x  x  e. Omni  ->  (
u  C_  { (/) }  ->  ( u  =  (/)  \/  u  =  { (/) } ) ) )
6665alrimiv 1799 . . 3  |-  ( A. x  x  e. Omni  ->  A. u
( u  C_  { (/) }  ->  ( u  =  (/)  \/  u  =  { (/)
} ) ) )
67 exmid01 3999 . . 3  |-  (EXMID  <->  A. u
( u  C_  { (/) }  ->  ( u  =  (/)  \/  u  =  { (/)
} ) ) )
6866, 67sylibr 132 . 2  |-  ( A. x  x  e. Omni  -> EXMID )
691, 68impbii 124 1  |-  (EXMID  <->  A. x  x  e. Omni )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 662   A.wal 1285    = wceq 1287   E.wex 1424    e. wcel 1436   A.wral 2355   E.wrex 2356   _Vcvv 2614    C_ wss 2986   (/)c0 3272   {csn 3425   {cpr 3426  EXMIDwem 3996    X. cxp 4402   -->wf 4968   ` cfv 4972   1oc1o 6109   2oc2o 6110  Omnicomni 6709
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-13 1447  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  ax-pr 4003  ax-un 4227
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2616  df-sbc 2829  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-br 3815  df-opab 3869  df-mpt 3870  df-exmid 3997  df-id 4087  df-suc 4165  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-fv 4980  df-1o 6116  df-2o 6117  df-omni 6711
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator