sup3exmid - Intuitionistic Logic Explorer

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

Theorem sup3exmid 8843

Description: If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.)

**Hypothesis**
Ref	Expression
sup3exmid.ex	$/\$ $/\$ $/\$

**Assertion**
Ref	Expression
sup3exmid	DECID

Distinct variable groups:

Proof of Theorem sup3exmid Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0lt1 8016	. . . 4
2		0re 7890	. . . . 5
3		1re 7889	. . . . 5
4		lttri3 7969	. . . . . . . 8 $/\$ $/\$
5	4	adantl 275	. . . . . . 7 $/\$ $/\$ $/\$
6		elrabi 2874	. . . . . . . . . . . 12 $\/$
7		elpri 3593	. . . . . . . . . . . 12 $\/$
8	6, 7	syl 14	. . . . . . . . . . 11 $\/$ $\/$
9		eleq1 2227	. . . . . . . . . . . . 13
10	2, 9	mpbiri 167	. . . . . . . . . . . 12
11		eleq1 2227	. . . . . . . . . . . . 13
12	3, 11	mpbiri 167	. . . . . . . . . . . 12
13	10, 12	jaoi 706	. . . . . . . . . . 11 $\/$
14	8, 13	syl 14	. . . . . . . . . 10 $\/$
15	14	ssriv 3141	. . . . . . . . 9 $\/$
16		eqid 2164	. . . . . . . . . . . 12
17	16	orci 721	. . . . . . . . . . 11 $\/$
18	2	elexi 2733	. . . . . . . . . . . . 13
19	18	prid1 3676	. . . . . . . . . . . 12
20		eqeq1 2171	. . . . . . . . . . . . . 14
21	20	orbi1d 781	. . . . . . . . . . . . 13 $\/$ $\/$
22	21	elrab3 2878	. . . . . . . . . . . 12 $\/$ $\/$
23	19, 22	ax-mp 5	. . . . . . . . . . 11 $\/$ $\/$
24	17, 23	mpbir 145	. . . . . . . . . 10 $\/$
25		elex2 2737	. . . . . . . . . 10 $\/$ $\/$
26	24, 25	ax-mp 5	. . . . . . . . 9 $\/$
27		elrabi 2874	. . . . . . . . . . . 12 $\/$
28		elpri 3593	. . . . . . . . . . . . 13 $\/$
29		0le1 8370	. . . . . . . . . . . . . . 15
30		breq1 3979	. . . . . . . . . . . . . . 15
31	29, 30	mpbiri 167	. . . . . . . . . . . . . 14
32	3	eqlei2 7984	. . . . . . . . . . . . . 14
33	31, 32	jaoi 706	. . . . . . . . . . . . 13 $\/$
34	28, 33	syl 14	. . . . . . . . . . . 12
35	27, 34	syl 14	. . . . . . . . . . 11 $\/$
36	35	rgen 2517	. . . . . . . . . 10 $\/$
37		breq2 3980	. . . . . . . . . . . 12
38	37	ralbidv 2464	. . . . . . . . . . 11 $\/$ $\/$
39	38	rspcev 2825	. . . . . . . . . 10 $/\$ $\/$ $\/$
40	3, 36, 39	mp2an 423	. . . . . . . . 9 $\/$
41		prexg 4183	. . . . . . . . . . . 12 $/\$
42	2, 3, 41	mp2an 423	. . . . . . . . . . 11
43	42	rabex 4120	. . . . . . . . . 10 $\/$
44		sseq1 3160	. . . . . . . . . . . 12 $\/$ $\/$
45		eleq2 2228	. . . . . . . . . . . . 13 $\/$ $\/$
46	45	exbidv 1812	. . . . . . . . . . . 12 $\/$ $\/$
47		raleq 2659	. . . . . . . . . . . . 13 $\/$ $\/$
48	47	rexbidv 2465	. . . . . . . . . . . 12 $\/$ $\/$
49	44, 46, 48	3anbi123d 1301	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
50		raleq 2659	. . . . . . . . . . . . 13 $\/$ $\/$
51		rexeq 2660	. . . . . . . . . . . . . . 15 $\/$ $\/$
52	51	imbi2d 229	. . . . . . . . . . . . . 14 $\/$ $\/$
53	52	ralbidv 2464	. . . . . . . . . . . . 13 $\/$ $\/$
54	50, 53	anbi12d 465	. . . . . . . . . . . 12 $\/$ $/\$ $\/$ $/\$ $\/$
55	54	rexbidv 2465	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $/\$ $\/$
56	49, 55	imbi12d 233	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
57		sup3exmid.ex	. . . . . . . . . 10 $/\$ $/\$ $/\$
58	43, 56, 57	vtocl 2775	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
59	15, 26, 40, 58	mp3an 1326	. . . . . . . 8 $\/$ $/\$ $\/$
60	59	a1i 9	. . . . . . 7 $\/$ $/\$ $\/$
61	5, 60	supclti 6954	. . . . . 6 $\/$
62	61	mptru 1351	. . . . 5 $\/$
63		axltwlin 7957	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
64	2, 3, 62, 63	mp3an 1326	. . . 4 $\/$ $\/$ $\/$
65	1, 64	ax-mp 5	. . 3 $\/$ $\/$ $\/$
66	5, 60	suplubti 6956	. . . . . . . 8 $/\$ $\/$ $\/$
67	66	mptru 1351	. . . . . . 7 $/\$ $\/$ $\/$
68	2, 67	mpan 421	. . . . . 6 $\/$ $\/$
69		df-rex 2448	. . . . . 6 $\/$ $\/$ $/\$
70	68, 69	sylib 121	. . . . 5 $\/$ $\/$ $/\$
71		eqeq1 2171	. . . . . . . . 9
72	71	orbi1d 781	. . . . . . . 8 $\/$ $\/$
73	72	elrab 2877	. . . . . . 7 $\/$ $/\$ $\/$
74		simpr 109	. . . . . . . . . 10 $/\$ $\/$ $/\$
75	74	gt0ne0d 8401	. . . . . . . . 9 $/\$ $\/$ $/\$
76	75	neneqd 2355	. . . . . . . 8 $/\$ $\/$ $/\$
77		simplr 520	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
78		orel1 715	. . . . . . . 8 $\/$
79	76, 77, 78	sylc 62	. . . . . . 7 $/\$ $\/$ $/\$
80	73, 79	sylanb 282	. . . . . 6 $\/$ $/\$
81	80	exlimiv 1585	. . . . 5 $\/$ $/\$
82	70, 81	syl 14	. . . 4 $\/$
83	3	ltnri 7982	. . . . . 6
84		iba 298	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
85	84	olcs 726	. . . . . . . . . . 11 $/\$ $\/$
86	73, 85	bitr4id 198	. . . . . . . . . 10 $\/$
87	86	eqrdv 2162	. . . . . . . . 9 $\/$
88	87	supeq1d 6943	. . . . . . . 8 $\/$
89	3	a1i 9	. . . . . . . . . 10
90	3	elexi 2733	. . . . . . . . . . . 12
91	90	prid2 3677	. . . . . . . . . . 11
92	91	a1i 9	. . . . . . . . . 10
93		elpri 3593	. . . . . . . . . . . 12 $\/$
94	2, 3	lenlti 7990	. . . . . . . . . . . . . . 15
95	29, 94	mpbi 144	. . . . . . . . . . . . . 14
96		breq2 3980	. . . . . . . . . . . . . 14
97	95, 96	mtbiri 665	. . . . . . . . . . . . 13
98		breq2 3980	. . . . . . . . . . . . . 14
99	83, 98	mtbiri 665	. . . . . . . . . . . . 13
100	97, 99	jaoi 706	. . . . . . . . . . . 12 $\/$
101	93, 100	syl 14	. . . . . . . . . . 11
102	101	adantl 275	. . . . . . . . . 10 $/\$
103	5, 89, 92, 102	supmaxti 6960	. . . . . . . . 9
104	103	mptru 1351	. . . . . . . 8
105	88, 104	eqtrdi 2213	. . . . . . 7 $\/$
106	105	breq1d 3986	. . . . . 6 $\/$
107	83, 106	mtbiri 665	. . . . 5 $\/$
108	107	con2i 617	. . . 4 $\/$
109	82, 108	orim12i 749	. . 3 $\/$ $\/$ $\/$ $\/$
110	65, 109	ax-mp 5	. 2 $\/$
111		df-dc 825	. 2 DECID $\/$
112	110, 111	mpbir 145	1 DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698 DECID wdc 824 $/\$ w3a 967

wceq 1342

wtru 1343

wex 1479

wcel 2135

wral 2442

wrex 2443

crab 2446

cvv 2721

wss 3111

cpr 3571 class class class wbr 3976

csup 6938

cr 7743

cc0 7744

c1 7745

clt 7924

cle 7925

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 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-13 2137 ax-14 2138 ax-ext 2146 ax-sep 4094 ax-pow 4147 ax-pr 4181 ax-un 4405 ax-setind 4508 ax-cnex 7835 ax-resscn 7836 ax-1re 7838 ax-addrcl 7841 ax-0lt1 7850 ax-rnegex 7853 ax-pre-ltirr 7856 ax-pre-ltwlin 7857 ax-pre-lttrn 7858 ax-pre-apti 7859

This theorem depends on definitions: df-bi 116 df-dc 825 df-3an 969 df-tru 1345 df-fal 1348 df-nf 1448 df-sb 1750 df-eu 2016 df-mo 2017 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ne 2335 df-nel 2430 df-ral 2447 df-rex 2448 df-reu 2449 df-rmo 2450 df-rab 2451 df-v 2723 df-sbc 2947 df-dif 3113 df-un 3115 df-in 3117 df-ss 3124 df-pw 3555 df-sn 3576 df-pr 3577 df-op 3579 df-uni 3784 df-br 3977 df-opab 4038 df-xp 4604 df-cnv 4606 df-iota 5147 df-riota 5792 df-sup 6940 df-pnf 7926 df-mnf 7927 df-xr 7928 df-ltxr 7929 df-le 7930

This theorem is referenced by: (None)

W3C validator