sup3exmid - Intuitionistic Logic Explorer

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

Theorem sup3exmid 9092

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 8261	. . . 4
2		0re 8134	. . . . 5
3		1re 8133	. . . . 5
4		lttri3 8214	. . . . . . . 8 $/\$ $/\$
5	4	adantl 277	. . . . . . 7 $/\$ $/\$ $/\$
6		elrabi 2956	. . . . . . . . . . . 12 $\/$
7		elpri 3689	. . . . . . . . . . . 12 $\/$
8	6, 7	syl 14	. . . . . . . . . . 11 $\/$ $\/$
9		eleq1 2292	. . . . . . . . . . . . 13
10	2, 9	mpbiri 168	. . . . . . . . . . . 12
11		eleq1 2292	. . . . . . . . . . . . 13
12	3, 11	mpbiri 168	. . . . . . . . . . . 12
13	10, 12	jaoi 721	. . . . . . . . . . 11 $\/$
14	8, 13	syl 14	. . . . . . . . . 10 $\/$
15	14	ssriv 3228	. . . . . . . . 9 $\/$
16		eqid 2229	. . . . . . . . . . . 12
17	16	orci 736	. . . . . . . . . . 11 $\/$
18	2	elexi 2812	. . . . . . . . . . . . 13
19	18	prid1 3772	. . . . . . . . . . . 12
20		eqeq1 2236	. . . . . . . . . . . . . 14
21	20	orbi1d 796	. . . . . . . . . . . . 13 $\/$ $\/$
22	21	elrab3 2960	. . . . . . . . . . . 12 $\/$ $\/$
23	19, 22	ax-mp 5	. . . . . . . . . . 11 $\/$ $\/$
24	17, 23	mpbir 146	. . . . . . . . . 10 $\/$
25		elex2 2816	. . . . . . . . . 10 $\/$ $\/$
26	24, 25	ax-mp 5	. . . . . . . . 9 $\/$
27		elrabi 2956	. . . . . . . . . . . 12 $\/$
28		elpri 3689	. . . . . . . . . . . . 13 $\/$
29		0le1 8616	. . . . . . . . . . . . . . 15
30		breq1 4085	. . . . . . . . . . . . . . 15
31	29, 30	mpbiri 168	. . . . . . . . . . . . . 14
32	3	eqlei2 8229	. . . . . . . . . . . . . 14
33	31, 32	jaoi 721	. . . . . . . . . . . . 13 $\/$
34	28, 33	syl 14	. . . . . . . . . . . 12
35	27, 34	syl 14	. . . . . . . . . . 11 $\/$
36	35	rgen 2583	. . . . . . . . . 10 $\/$
37		breq2 4086	. . . . . . . . . . . 12
38	37	ralbidv 2530	. . . . . . . . . . 11 $\/$ $\/$
39	38	rspcev 2907	. . . . . . . . . 10 $/\$ $\/$ $\/$
40	3, 36, 39	mp2an 426	. . . . . . . . 9 $\/$
41		prexg 4294	. . . . . . . . . . . 12 $/\$
42	2, 3, 41	mp2an 426	. . . . . . . . . . 11
43	42	rabex 4227	. . . . . . . . . 10 $\/$
44		sseq1 3247	. . . . . . . . . . . 12 $\/$ $\/$
45		eleq2 2293	. . . . . . . . . . . . 13 $\/$ $\/$
46	45	exbidv 1871	. . . . . . . . . . . 12 $\/$ $\/$
47		raleq 2728	. . . . . . . . . . . . 13 $\/$ $\/$
48	47	rexbidv 2531	. . . . . . . . . . . 12 $\/$ $\/$
49	44, 46, 48	3anbi123d 1346	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
50		raleq 2728	. . . . . . . . . . . . 13 $\/$ $\/$
51		rexeq 2729	. . . . . . . . . . . . . . 15 $\/$ $\/$
52	51	imbi2d 230	. . . . . . . . . . . . . 14 $\/$ $\/$
53	52	ralbidv 2530	. . . . . . . . . . . . 13 $\/$ $\/$
54	50, 53	anbi12d 473	. . . . . . . . . . . 12 $\/$ $/\$ $\/$ $/\$ $\/$
55	54	rexbidv 2531	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $/\$ $\/$
56	49, 55	imbi12d 234	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
57		sup3exmid.ex	. . . . . . . . . 10 $/\$ $/\$ $/\$
58	43, 56, 57	vtocl 2855	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
59	15, 26, 40, 58	mp3an 1371	. . . . . . . 8 $\/$ $/\$ $\/$
60	59	a1i 9	. . . . . . 7 $\/$ $/\$ $\/$
61	5, 60	supclti 7153	. . . . . 6 $\/$
62	61	mptru 1404	. . . . 5 $\/$
63		axltwlin 8202	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
64	2, 3, 62, 63	mp3an 1371	. . . 4 $\/$ $\/$ $\/$
65	1, 64	ax-mp 5	. . 3 $\/$ $\/$ $\/$
66	5, 60	suplubti 7155	. . . . . . . 8 $/\$ $\/$ $\/$
67	66	mptru 1404	. . . . . . 7 $/\$ $\/$ $\/$
68	2, 67	mpan 424	. . . . . 6 $\/$ $\/$
69		df-rex 2514	. . . . . 6 $\/$ $\/$ $/\$
70	68, 69	sylib 122	. . . . 5 $\/$ $\/$ $/\$
71		eqeq1 2236	. . . . . . . . 9
72	71	orbi1d 796	. . . . . . . 8 $\/$ $\/$
73	72	elrab 2959	. . . . . . 7 $\/$ $/\$ $\/$
74		simpr 110	. . . . . . . . . 10 $/\$ $\/$ $/\$
75	74	gt0ne0d 8647	. . . . . . . . 9 $/\$ $\/$ $/\$
76	75	neneqd 2421	. . . . . . . 8 $/\$ $\/$ $/\$
77		simplr 528	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
78		orel1 730	. . . . . . . 8 $\/$
79	76, 77, 78	sylc 62	. . . . . . 7 $/\$ $\/$ $/\$
80	73, 79	sylanb 284	. . . . . 6 $\/$ $/\$
81	80	exlimiv 1644	. . . . 5 $\/$ $/\$
82	70, 81	syl 14	. . . 4 $\/$
83	3	ltnri 8227	. . . . . 6
84		iba 300	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
85	84	olcs 741	. . . . . . . . . . 11 $/\$ $\/$
86	73, 85	bitr4id 199	. . . . . . . . . 10 $\/$
87	86	eqrdv 2227	. . . . . . . . 9 $\/$
88	87	supeq1d 7142	. . . . . . . 8 $\/$
89	3	a1i 9	. . . . . . . . . 10
90	3	elexi 2812	. . . . . . . . . . . 12
91	90	prid2 3773	. . . . . . . . . . 11
92	91	a1i 9	. . . . . . . . . 10
93		elpri 3689	. . . . . . . . . . . 12 $\/$
94	2, 3	lenlti 8235	. . . . . . . . . . . . . . 15
95	29, 94	mpbi 145	. . . . . . . . . . . . . 14
96		breq2 4086	. . . . . . . . . . . . . 14
97	95, 96	mtbiri 679	. . . . . . . . . . . . 13
98		breq2 4086	. . . . . . . . . . . . . 14
99	83, 98	mtbiri 679	. . . . . . . . . . . . 13
100	97, 99	jaoi 721	. . . . . . . . . . . 12 $\/$
101	93, 100	syl 14	. . . . . . . . . . 11
102	101	adantl 277	. . . . . . . . . 10 $/\$
103	5, 89, 92, 102	supmaxti 7159	. . . . . . . . 9
104	103	mptru 1404	. . . . . . . 8
105	88, 104	eqtrdi 2278	. . . . . . 7 $\/$
106	105	breq1d 4092	. . . . . 6 $\/$
107	83, 106	mtbiri 679	. . . . 5 $\/$
108	107	con2i 630	. . . 4 $\/$
109	82, 108	orim12i 764	. . 3 $\/$ $\/$ $\/$ $\/$
110	65, 109	ax-mp 5	. 2 $\/$
111		df-dc 840	. 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 713 DECID wdc 839 $/\$ w3a 1002

wceq 1395

wtru 1396

wex 1538

wcel 2200

wral 2508

wrex 2509

crab 2512

cvv 2799

wss 3197

cpr 3667 class class class wbr 4082

csup 7137

cr 7986

cc0 7987

c1 7988

clt 8169

cle 8170

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4201 ax-pow 4257 ax-pr 4292 ax-un 4521 ax-setind 4626 ax-cnex 8078 ax-resscn 8079 ax-1re 8081 ax-addrcl 8084 ax-0lt1 8093 ax-rnegex 8096 ax-pre-ltirr 8099 ax-pre-ltwlin 8100 ax-pre-lttrn 8101 ax-pre-apti 8102

This theorem depends on definitions: df-bi 117 df-dc 840 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-br 4083 df-opab 4145 df-xp 4722 df-cnv 4724 df-iota 5274 df-riota 5947 df-sup 7139 df-pnf 8171 df-mnf 8172 df-xr 8173 df-ltxr 8174 df-le 8175

This theorem is referenced by: (None)

W3C validator