sup3exmid - Intuitionistic Logic Explorer

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

Theorem sup3exmid 8903

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 8074	. . . 4
2		0re 7948	. . . . 5
3		1re 7947	. . . . 5
4		lttri3 8027	. . . . . . . 8 $/\$ $/\$
5	4	adantl 277	. . . . . . 7 $/\$ $/\$ $/\$
6		elrabi 2890	. . . . . . . . . . . 12 $\/$
7		elpri 3614	. . . . . . . . . . . 12 $\/$
8	6, 7	syl 14	. . . . . . . . . . 11 $\/$ $\/$
9		eleq1 2240	. . . . . . . . . . . . 13
10	2, 9	mpbiri 168	. . . . . . . . . . . 12
11		eleq1 2240	. . . . . . . . . . . . 13
12	3, 11	mpbiri 168	. . . . . . . . . . . 12
13	10, 12	jaoi 716	. . . . . . . . . . 11 $\/$
14	8, 13	syl 14	. . . . . . . . . 10 $\/$
15	14	ssriv 3159	. . . . . . . . 9 $\/$
16		eqid 2177	. . . . . . . . . . . 12
17	16	orci 731	. . . . . . . . . . 11 $\/$
18	2	elexi 2749	. . . . . . . . . . . . 13
19	18	prid1 3697	. . . . . . . . . . . 12
20		eqeq1 2184	. . . . . . . . . . . . . 14
21	20	orbi1d 791	. . . . . . . . . . . . 13 $\/$ $\/$
22	21	elrab3 2894	. . . . . . . . . . . 12 $\/$ $\/$
23	19, 22	ax-mp 5	. . . . . . . . . . 11 $\/$ $\/$
24	17, 23	mpbir 146	. . . . . . . . . 10 $\/$
25		elex2 2753	. . . . . . . . . 10 $\/$ $\/$
26	24, 25	ax-mp 5	. . . . . . . . 9 $\/$
27		elrabi 2890	. . . . . . . . . . . 12 $\/$
28		elpri 3614	. . . . . . . . . . . . 13 $\/$
29		0le1 8428	. . . . . . . . . . . . . . 15
30		breq1 4003	. . . . . . . . . . . . . . 15
31	29, 30	mpbiri 168	. . . . . . . . . . . . . 14
32	3	eqlei2 8042	. . . . . . . . . . . . . 14
33	31, 32	jaoi 716	. . . . . . . . . . . . 13 $\/$
34	28, 33	syl 14	. . . . . . . . . . . 12
35	27, 34	syl 14	. . . . . . . . . . 11 $\/$
36	35	rgen 2530	. . . . . . . . . 10 $\/$
37		breq2 4004	. . . . . . . . . . . 12
38	37	ralbidv 2477	. . . . . . . . . . 11 $\/$ $\/$
39	38	rspcev 2841	. . . . . . . . . 10 $/\$ $\/$ $\/$
40	3, 36, 39	mp2an 426	. . . . . . . . 9 $\/$
41		prexg 4208	. . . . . . . . . . . 12 $/\$
42	2, 3, 41	mp2an 426	. . . . . . . . . . 11
43	42	rabex 4144	. . . . . . . . . 10 $\/$
44		sseq1 3178	. . . . . . . . . . . 12 $\/$ $\/$
45		eleq2 2241	. . . . . . . . . . . . 13 $\/$ $\/$
46	45	exbidv 1825	. . . . . . . . . . . 12 $\/$ $\/$
47		raleq 2672	. . . . . . . . . . . . 13 $\/$ $\/$
48	47	rexbidv 2478	. . . . . . . . . . . 12 $\/$ $\/$
49	44, 46, 48	3anbi123d 1312	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
50		raleq 2672	. . . . . . . . . . . . 13 $\/$ $\/$
51		rexeq 2673	. . . . . . . . . . . . . . 15 $\/$ $\/$
52	51	imbi2d 230	. . . . . . . . . . . . . 14 $\/$ $\/$
53	52	ralbidv 2477	. . . . . . . . . . . . 13 $\/$ $\/$
54	50, 53	anbi12d 473	. . . . . . . . . . . 12 $\/$ $/\$ $\/$ $/\$ $\/$
55	54	rexbidv 2478	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $/\$ $\/$
56	49, 55	imbi12d 234	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
57		sup3exmid.ex	. . . . . . . . . 10 $/\$ $/\$ $/\$
58	43, 56, 57	vtocl 2791	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
59	15, 26, 40, 58	mp3an 1337	. . . . . . . 8 $\/$ $/\$ $\/$
60	59	a1i 9	. . . . . . 7 $\/$ $/\$ $\/$
61	5, 60	supclti 6991	. . . . . 6 $\/$
62	61	mptru 1362	. . . . 5 $\/$
63		axltwlin 8015	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
64	2, 3, 62, 63	mp3an 1337	. . . 4 $\/$ $\/$ $\/$
65	1, 64	ax-mp 5	. . 3 $\/$ $\/$ $\/$
66	5, 60	suplubti 6993	. . . . . . . 8 $/\$ $\/$ $\/$
67	66	mptru 1362	. . . . . . 7 $/\$ $\/$ $\/$
68	2, 67	mpan 424	. . . . . 6 $\/$ $\/$
69		df-rex 2461	. . . . . 6 $\/$ $\/$ $/\$
70	68, 69	sylib 122	. . . . 5 $\/$ $\/$ $/\$
71		eqeq1 2184	. . . . . . . . 9
72	71	orbi1d 791	. . . . . . . 8 $\/$ $\/$
73	72	elrab 2893	. . . . . . 7 $\/$ $/\$ $\/$
74		simpr 110	. . . . . . . . . 10 $/\$ $\/$ $/\$
75	74	gt0ne0d 8459	. . . . . . . . 9 $/\$ $\/$ $/\$
76	75	neneqd 2368	. . . . . . . 8 $/\$ $\/$ $/\$
77		simplr 528	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
78		orel1 725	. . . . . . . 8 $\/$
79	76, 77, 78	sylc 62	. . . . . . 7 $/\$ $\/$ $/\$
80	73, 79	sylanb 284	. . . . . 6 $\/$ $/\$
81	80	exlimiv 1598	. . . . 5 $\/$ $/\$
82	70, 81	syl 14	. . . 4 $\/$
83	3	ltnri 8040	. . . . . 6
84		iba 300	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
85	84	olcs 736	. . . . . . . . . . 11 $/\$ $\/$
86	73, 85	bitr4id 199	. . . . . . . . . 10 $\/$
87	86	eqrdv 2175	. . . . . . . . 9 $\/$
88	87	supeq1d 6980	. . . . . . . 8 $\/$
89	3	a1i 9	. . . . . . . . . 10
90	3	elexi 2749	. . . . . . . . . . . 12
91	90	prid2 3698	. . . . . . . . . . 11
92	91	a1i 9	. . . . . . . . . 10
93		elpri 3614	. . . . . . . . . . . 12 $\/$
94	2, 3	lenlti 8048	. . . . . . . . . . . . . . 15
95	29, 94	mpbi 145	. . . . . . . . . . . . . 14
96		breq2 4004	. . . . . . . . . . . . . 14
97	95, 96	mtbiri 675	. . . . . . . . . . . . 13
98		breq2 4004	. . . . . . . . . . . . . 14
99	83, 98	mtbiri 675	. . . . . . . . . . . . 13
100	97, 99	jaoi 716	. . . . . . . . . . . 12 $\/$
101	93, 100	syl 14	. . . . . . . . . . 11
102	101	adantl 277	. . . . . . . . . 10 $/\$
103	5, 89, 92, 102	supmaxti 6997	. . . . . . . . 9
104	103	mptru 1362	. . . . . . . 8
105	88, 104	eqtrdi 2226	. . . . . . 7 $\/$
106	105	breq1d 4010	. . . . . 6 $\/$
107	83, 106	mtbiri 675	. . . . 5 $\/$
108	107	con2i 627	. . . 4 $\/$
109	82, 108	orim12i 759	. . 3 $\/$ $\/$ $\/$ $\/$
110	65, 109	ax-mp 5	. 2 $\/$
111		df-dc 835	. 2 DECID $\/$
112	110, 111	mpbir 146	1 DECID

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 708 DECID wdc 834 $/\$ w3a 978

wceq 1353

wtru 1354

wex 1492

wcel 2148

wral 2455

wrex 2456

crab 2459

cvv 2737

wss 3129

cpr 3592 class class class wbr 4000

csup 6975

cr 7801

cc0 7802

c1 7803

clt 7982

cle 7983

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4118 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-cnex 7893 ax-resscn 7894 ax-1re 7896 ax-addrcl 7899 ax-0lt1 7908 ax-rnegex 7911 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917

This theorem depends on definitions: df-bi 117 df-dc 835 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-br 4001 df-opab 4062 df-xp 4629 df-cnv 4631 df-iota 5174 df-riota 5825 df-sup 6977 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988

This theorem is referenced by: (None)

W3C validator