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

Theorem exmidomni 7118
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 7117 . 2  |-  (EXMID  ->  A. x  x  e. Omni )
2 vex 2733 . . . . . . . . . 10  |-  u  e. 
_V
3 eleq1w 2231 . . . . . . . . . 10  |-  ( x  =  u  ->  (
x  e. Omni  <->  u  e. Omni ) )
42, 3spcv 2824 . . . . . . . . 9  |-  ( A. x  x  e. Omni  ->  u  e. Omni )
5 xpeq1 4625 . . . . . . . . . . . . . 14  |-  ( x  =  u  ->  (
x  X.  { (/) } )  =  ( u  X.  { (/) } ) )
65fveq1d 5498 . . . . . . . . . . . . 13  |-  ( x  =  u  ->  (
( x  X.  { (/)
} ) `  y
)  =  ( ( u  X.  { (/) } ) `  y ) )
76eqeq1d 2179 . . . . . . . . . . . 12  |-  ( x  =  u  ->  (
( ( x  X.  { (/) } ) `  y )  =  (/)  <->  (
( u  X.  { (/)
} ) `  y
)  =  (/) ) )
87rexeqbi1dv 2674 . . . . . . . . . . 11  |-  ( x  =  u  ->  ( E. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  (/)  <->  E. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  (/) ) )
96eqeq1d 2179 . . . . . . . . . . . 12  |-  ( x  =  u  ->  (
( ( x  X.  { (/) } ) `  y )  =  1o  <->  ( ( u  X.  { (/)
} ) `  y
)  =  1o ) )
109raleqbi1dv 2673 . . . . . . . . . . 11  |-  ( x  =  u  ->  ( A. y  e.  x  ( ( x  X.  { (/) } ) `  y )  =  1o  <->  A. y  e.  u  ( ( u  X.  { (/)
} ) `  y
)  =  1o ) )
118, 10orbi12d 788 . . . . . . . . . 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 2733 . . . . . . . . . . . . 13  |-  x  e. 
_V
13 isomni 7112 . . . . . . . . . . . . 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 5 . . . . . . . . . . . 12  |-  ( x  e. Omni 
<-> 
A. f ( f : x --> 2o  ->  ( E. y  e.  x  ( f `  y
)  =  (/)  \/  A. y  e.  x  (
f `  y )  =  1o ) ) )
1514biimpi 119 . . . . . . . . . . 11  |-  ( x  e. Omni  ->  A. f ( f : x --> 2o  ->  ( E. y  e.  x  ( f `  y
)  =  (/)  \/  A. y  e.  x  (
f `  y )  =  1o ) ) )
16 0ex 4116 . . . . . . . . . . . . . 14  |-  (/)  e.  _V
1716prid1 3689 . . . . . . . . . . . . 13  |-  (/)  e.  { (/)
,  1o }
18 df2o3 6409 . . . . . . . . . . . . 13  |-  2o  =  { (/) ,  1o }
1917, 18eleqtrri 2246 . . . . . . . . . . . 12  |-  (/)  e.  2o
2019fconst6 5397 . . . . . . . . . . 11  |-  ( x  X.  { (/) } ) : x --> 2o
21 p0ex 4174 . . . . . . . . . . . . 13  |-  { (/) }  e.  _V
2212, 21xpex 4726 . . . . . . . . . . . 12  |-  ( x  X.  { (/) } )  e.  _V
23 feq1 5330 . . . . . . . . . . . . 13  |-  ( f  =  ( x  X.  { (/) } )  -> 
( f : x --> 2o  <->  ( x  X.  { (/) } ) : x --> 2o ) )
24 fveq1 5495 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( x  X.  { (/) } )  -> 
( f `  y
)  =  ( ( x  X.  { (/) } ) `  y ) )
2524eqeq1d 2179 . . . . . . . . . . . . . . 15  |-  ( f  =  ( x  X.  { (/) } )  -> 
( ( f `  y )  =  (/)  <->  (
( x  X.  { (/)
} ) `  y
)  =  (/) ) )
2625rexbidv 2471 . . . . . . . . . . . . . 14  |-  ( f  =  ( x  X.  { (/) } )  -> 
( E. y  e.  x  ( f `  y )  =  (/)  <->  E. y  e.  x  (
( x  X.  { (/)
} ) `  y
)  =  (/) ) )
2724eqeq1d 2179 . . . . . . . . . . . . . . 15  |-  ( f  =  ( x  X.  { (/) } )  -> 
( ( f `  y )  =  1o  <->  ( ( x  X.  { (/)
} ) `  y
)  =  1o ) )
2827ralbidv 2470 . . . . . . . . . . . . . 14  |-  ( f  =  ( x  X.  { (/) } )  -> 
( A. y  e.  x  ( f `  y )  =  1o  <->  A. y  e.  x  ( ( x  X.  { (/)
} ) `  y
)  =  1o ) )
2926, 28orbi12d 788 . . . . . . . . . . . . 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 233 . . . . . . . . . . . 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 2824 . . . . . . . . . . 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 1439 . . . . . . . . . 10  |-  ( x  e. Omni  ->  ( E. y  e.  x  ( (
x  X.  { (/) } ) `  y )  =  (/)  \/  A. y  e.  x  ( (
x  X.  { (/) } ) `  y )  =  1o ) )
3311, 32vtoclga 2796 . . . . . . . . 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 274 . . . . . . 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 525 . . . . . . . . . 10  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  E. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  (/) )  ->  u  C_ 
{ (/) } )
37 rexm 3514 . . . . . . . . . . . 12  |-  ( E. y  e.  u  ( ( u  X.  { (/)
} ) `  y
)  =  (/)  ->  E. y 
y  e.  u )
38 sssnm 3741 . . . . . . . . . . . 12  |-  ( E. y  y  e.  u  ->  ( u  C_  { (/) }  <-> 
u  =  { (/) } ) )
3937, 38syl 14 . . . . . . . . . . 11  |-  ( E. y  e.  u  ( ( u  X.  { (/)
} ) `  y
)  =  (/)  ->  (
u  C_  { (/) }  <->  u  =  { (/) } ) )
4039adantl 275 . . . . . . . . . 10  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  E. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  (/) )  ->  (
u  C_  { (/) }  <->  u  =  { (/) } ) )
4136, 40mpbid 146 . . . . . . . . 9  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  E. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  (/) )  ->  u  =  { (/) } )
4241ex 114 . . . . . . . 8  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( E. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  (/)  ->  u  =  { (/) } ) )
43 nfv 1521 . . . . . . . . . . . 12  |-  F/ y ( A. x  x  e. Omni  /\  u  C_  { (/) } )
44 nfra1 2501 . . . . . . . . . . . 12  |-  F/ y A. y  e.  u  ( ( u  X.  { (/) } ) `  y )  =  1o
4543, 44nfan 1558 . . . . . . . . . . 11  |-  F/ y ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )
46 nfcv 2312 . . . . . . . . . . 11  |-  F/_ y
u
47 nfcv 2312 . . . . . . . . . . 11  |-  F/_ y (/)
48 1n0 6411 . . . . . . . . . . . . . 14  |-  1o  =/=  (/)
4948neii 2342 . . . . . . . . . . . . 13  |-  -.  1o  =  (/)
50 simpr 109 . . . . . . . . . . . . . . . 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 2558 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )  /\  y  e.  u
)  ->  ( (
u  X.  { (/) } ) `  y )  =  1o )
5216fvconst2 5712 . . . . . . . . . . . . . . . 16  |-  ( y  e.  u  ->  (
( u  X.  { (/)
} ) `  y
)  =  (/) )
5352adantl 275 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )  /\  y  e.  u
)  ->  ( (
u  X.  { (/) } ) `  y )  =  (/) )
5451, 53eqtr3d 2205 . . . . . . . . . . . . . 14  |-  ( ( ( ( A. x  x  e. Omni  /\  u  C_  {
(/) } )  /\  A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o )  /\  y  e.  u
)  ->  1o  =  (/) )
5554ex 114 . . . . . . . . . . . . 13  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  -> 
( y  e.  u  ->  1o  =  (/) ) )
5649, 55mtoi 659 . . . . . . . . . . . 12  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  ->  -.  y  e.  u
)
5756pm2.21d 614 . . . . . . . . . . 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 3152 . . . . . . . . . 10  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  ->  u  C_  (/) )
59 ss0 3455 . . . . . . . . . 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 114 . . . . . . . 8  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( A. y  e.  u  (
( u  X.  { (/)
} ) `  y
)  =  1o  ->  u  =  (/) ) )
6242, 61orim12d 781 . . . . . . 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 724 . . . . 5  |-  ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  ->  ( u  =  (/)  \/  u  =  { (/) } ) )
6564ex 114 . . . 4  |-  ( A. x  x  e. Omni  ->  (
u  C_  { (/) }  ->  ( u  =  (/)  \/  u  =  { (/) } ) ) )
6665alrimiv 1867 . . 3  |-  ( A. x  x  e. Omni  ->  A. u
( u  C_  { (/) }  ->  ( u  =  (/)  \/  u  =  { (/)
} ) ) )
67 exmid01 4184 . . 3  |-  (EXMID  <->  A. u
( u  C_  { (/) }  ->  ( u  =  (/)  \/  u  =  { (/)
} ) ) )
6866, 67sylibr 133 . 2  |-  ( A. x  x  e. Omni  -> EXMID )
691, 68impbii 125 1  |-  (EXMID  <->  A. x  x  e. Omni )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 703   A.wal 1346    = wceq 1348   E.wex 1485    e. wcel 2141   A.wral 2448   E.wrex 2449   _Vcvv 2730    C_ wss 3121   (/)c0 3414   {csn 3583   {cpr 3584  EXMIDwem 4180    X. cxp 4609   -->wf 5194   ` cfv 5198   1oc1o 6388   2oc2o 6389  Omnicomni 7110
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-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-mpt 4052  df-exmid 4181  df-id 4278  df-suc 4356  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-fv 5206  df-1o 6395  df-2o 6396  df-omni 7111
This theorem is referenced by:  exmidlpo  7119
  Copyright terms: Public domain W3C validator