Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > acexmid | Unicode version |
Description: The axiom of choice
implies excluded middle. Theorem 1.3 in [Bauer]
p. 483.
The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function provides a value when is inhabited (as opposed to non-empty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). (Contributed by Jim Kingdon, 4-Aug-2019.) |
Ref | Expression |
---|---|
acexmid.choice |
Ref | Expression |
---|---|
acexmid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1421 | . . . . . . . . . . . . . 14 | |
2 | 1 | sb8eu 1913 | . . . . . . . . . . . . 13 |
3 | eleq12 2102 | . . . . . . . . . . . . . . . . . . . 20 | |
4 | 3 | ancoms 255 | . . . . . . . . . . . . . . . . . . 19 |
5 | 4 | 3adant3 924 | . . . . . . . . . . . . . . . . . 18 |
6 | eleq12 2102 | . . . . . . . . . . . . . . . . . . . . 21 | |
7 | 6 | 3ad2antl1 1066 | . . . . . . . . . . . . . . . . . . . 20 |
8 | eleq12 2102 | . . . . . . . . . . . . . . . . . . . . 21 | |
9 | 8 | 3ad2antl2 1067 | . . . . . . . . . . . . . . . . . . . 20 |
10 | 7, 9 | anbi12d 442 | . . . . . . . . . . . . . . . . . . 19 |
11 | simpl3 909 | . . . . . . . . . . . . . . . . . . 19 | |
12 | 10, 11 | cbvrexdva2 2538 | . . . . . . . . . . . . . . . . . 18 |
13 | 5, 12 | anbi12d 442 | . . . . . . . . . . . . . . . . 17 |
14 | 13 | 3com23 1110 | . . . . . . . . . . . . . . . 16 |
15 | 14 | 3expa 1104 | . . . . . . . . . . . . . . 15 |
16 | 15 | sbiedv 1672 | . . . . . . . . . . . . . 14 |
17 | 16 | eubidv 1908 | . . . . . . . . . . . . 13 |
18 | 2, 17 | syl5bb 181 | . . . . . . . . . . . 12 |
19 | df-reu 2313 | . . . . . . . . . . . 12 | |
20 | df-reu 2313 | . . . . . . . . . . . 12 | |
21 | 18, 19, 20 | 3bitr4g 212 | . . . . . . . . . . 11 |
22 | 21 | adantr 261 | . . . . . . . . . 10 |
23 | simpll 481 | . . . . . . . . . 10 | |
24 | 22, 23 | cbvraldva2 2537 | . . . . . . . . 9 |
25 | 24 | ancoms 255 | . . . . . . . 8 |
26 | 25 | adantll 445 | . . . . . . 7 |
27 | simpll 481 | . . . . . . 7 | |
28 | 26, 27 | cbvraldva2 2537 | . . . . . 6 |
29 | 28 | cbvexdva 1804 | . . . . 5 |
30 | 29 | cbvalv 1794 | . . . 4 |
31 | acexmid.choice | . . . 4 | |
32 | 30, 31 | mpgbir 1342 | . . 3 |
33 | 32 | spi 1429 | . 2 |
34 | 33 | acexmidlemv 5510 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wa 97 wb 98 wo 629 w3a 885 wal 1241 wex 1381 wsb 1645 weu 1900 wral 2306 wrex 2307 wreu 2308 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-sep 3875 ax-nul 3883 ax-pow 3927 ax-pr 3944 |
This theorem depends on definitions: df-bi 110 df-3or 886 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-eu 1903 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ral 2311 df-rex 2312 df-reu 2313 df-rab 2315 df-v 2559 df-sbc 2765 df-dif 2920 df-un 2922 df-in 2924 df-ss 2931 df-nul 3225 df-pw 3361 df-sn 3381 df-pr 3382 df-uni 3581 df-tr 3855 df-iord 4103 df-on 4105 df-suc 4108 df-iota 4867 df-riota 5468 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |