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

Theorem exmidomni 6742
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 6741 . 2  |-  (EXMID  ->  A. x  x  e. Omni )
2 vex 2618 . . . . . . . . . 10  |-  u  e. 
_V
3 eleq1w 2145 . . . . . . . . . 10  |-  ( x  =  u  ->  (
x  e. Omni  <->  u  e. Omni ) )
42, 3spcv 2705 . . . . . . . . 9  |-  ( A. x  x  e. Omni  ->  u  e. Omni )
5 xpeq1 4425 . . . . . . . . . . . . . 14  |-  ( x  =  u  ->  (
x  X.  { (/) } )  =  ( u  X.  { (/) } ) )
65fveq1d 5270 . . . . . . . . . . . . 13  |-  ( x  =  u  ->  (
( x  X.  { (/)
} ) `  y
)  =  ( ( u  X.  { (/) } ) `  y ) )
76eqeq1d 2093 . . . . . . . . . . . 12  |-  ( x  =  u  ->  (
( ( x  X.  { (/) } ) `  y )  =  (/)  <->  (
( u  X.  { (/)
} ) `  y
)  =  (/) ) )
87rexeqbi1dv 2567 . . . . . . . . . . 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 2566 . . . . . . . . . . 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 2618 . . . . . . . . . . . . 13  |-  x  e. 
_V
13 isomni 6736 . . . . . . . . . . . . 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 3941 . . . . . . . . . . . . . 14  |-  (/)  e.  _V
1716prid1 3531 . . . . . . . . . . . . 13  |-  (/)  e.  { (/)
,  1o }
18 df2o3 6149 . . . . . . . . . . . . 13  |-  2o  =  { (/) ,  1o }
1917, 18eleqtrri 2160 . . . . . . . . . . . 12  |-  (/)  e.  2o
2019fconst6 5173 . . . . . . . . . . 11  |-  ( x  X.  { (/) } ) : x --> 2o
21 p0ex 3997 . . . . . . . . . . . . 13  |-  { (/) }  e.  _V
2212, 21xpex 4521 . . . . . . . . . . . 12  |-  ( x  X.  { (/) } )  e.  _V
23 feq1 5110 . . . . . . . . . . . . 13  |-  ( f  =  ( x  X.  { (/) } )  -> 
( f : x --> 2o  <->  ( x  X.  { (/) } ) : x --> 2o ) )
24 fveq1 5267 . . . . . . . . . . . . . . . 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 2705 . . . . . . . . . . 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 2678 . . . . . . . . 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 3368 . . . . . . . . . . . 12  |-  ( E. y  e.  u  ( ( u  X.  { (/)
} ) `  y
)  =  (/)  ->  E. y 
y  e.  u )
38 sssnm 3581 . . . . . . . . . . . 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 6151 . . . . . . . . . . . . . 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 5474 . . . . . . . . . . . . . . . 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 3019 . . . . . . . . . 10  |-  ( ( ( A. x  x  e. Omni  /\  u  C_  { (/) } )  /\  A. y  e.  u  ( (
u  X.  { (/) } ) `  y )  =  1o )  ->  u  C_  (/) )
59 ss0 3311 . . . . . . . . . 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 4006 . . 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 2615    C_ wss 2988   (/)c0 3275   {csn 3431   {cpr 3432  EXMIDwem 4003    X. cxp 4409   -->wf 4977   ` cfv 4981   1oc1o 6128   2oc2o 6129  Omnicomni 6732
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 3932  ax-nul 3940  ax-pow 3984  ax-pr 4010  ax-un 4234
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 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-opab 3875  df-mpt 3876  df-exmid 4004  df-id 4094  df-suc 4172  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-rn 4422  df-iota 4946  df-fun 4983  df-fn 4984  df-f 4985  df-fv 4989  df-1o 6135  df-2o 6136  df-omni 6734
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator