sup3exmid - Intuitionistic Logic Explorer

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

Theorem sup3exmid 9043

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 8212	. . . 4
2		0re 8085	. . . . 5
3		1re 8084	. . . . 5
4		lttri3 8165	. . . . . . . 8 $/\$ $/\$
5	4	adantl 277	. . . . . . 7 $/\$ $/\$ $/\$
6		elrabi 2928	. . . . . . . . . . . 12 $\/$
7		elpri 3658	. . . . . . . . . . . 12 $\/$
8	6, 7	syl 14	. . . . . . . . . . 11 $\/$ $\/$
9		eleq1 2269	. . . . . . . . . . . . 13
10	2, 9	mpbiri 168	. . . . . . . . . . . 12
11		eleq1 2269	. . . . . . . . . . . . 13
12	3, 11	mpbiri 168	. . . . . . . . . . . 12
13	10, 12	jaoi 718	. . . . . . . . . . 11 $\/$
14	8, 13	syl 14	. . . . . . . . . 10 $\/$
15	14	ssriv 3199	. . . . . . . . 9 $\/$
16		eqid 2206	. . . . . . . . . . . 12
17	16	orci 733	. . . . . . . . . . 11 $\/$
18	2	elexi 2786	. . . . . . . . . . . . 13
19	18	prid1 3741	. . . . . . . . . . . 12
20		eqeq1 2213	. . . . . . . . . . . . . 14
21	20	orbi1d 793	. . . . . . . . . . . . 13 $\/$ $\/$
22	21	elrab3 2932	. . . . . . . . . . . 12 $\/$ $\/$
23	19, 22	ax-mp 5	. . . . . . . . . . 11 $\/$ $\/$
24	17, 23	mpbir 146	. . . . . . . . . 10 $\/$
25		elex2 2790	. . . . . . . . . 10 $\/$ $\/$
26	24, 25	ax-mp 5	. . . . . . . . 9 $\/$
27		elrabi 2928	. . . . . . . . . . . 12 $\/$
28		elpri 3658	. . . . . . . . . . . . 13 $\/$
29		0le1 8567	. . . . . . . . . . . . . . 15
30		breq1 4051	. . . . . . . . . . . . . . 15
31	29, 30	mpbiri 168	. . . . . . . . . . . . . 14
32	3	eqlei2 8180	. . . . . . . . . . . . . 14
33	31, 32	jaoi 718	. . . . . . . . . . . . 13 $\/$
34	28, 33	syl 14	. . . . . . . . . . . 12
35	27, 34	syl 14	. . . . . . . . . . 11 $\/$
36	35	rgen 2560	. . . . . . . . . 10 $\/$
37		breq2 4052	. . . . . . . . . . . 12
38	37	ralbidv 2507	. . . . . . . . . . 11 $\/$ $\/$
39	38	rspcev 2879	. . . . . . . . . 10 $/\$ $\/$ $\/$
40	3, 36, 39	mp2an 426	. . . . . . . . 9 $\/$
41		prexg 4260	. . . . . . . . . . . 12 $/\$
42	2, 3, 41	mp2an 426	. . . . . . . . . . 11
43	42	rabex 4193	. . . . . . . . . 10 $\/$
44		sseq1 3218	. . . . . . . . . . . 12 $\/$ $\/$
45		eleq2 2270	. . . . . . . . . . . . 13 $\/$ $\/$
46	45	exbidv 1849	. . . . . . . . . . . 12 $\/$ $\/$
47		raleq 2703	. . . . . . . . . . . . 13 $\/$ $\/$
48	47	rexbidv 2508	. . . . . . . . . . . 12 $\/$ $\/$
49	44, 46, 48	3anbi123d 1325	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
50		raleq 2703	. . . . . . . . . . . . 13 $\/$ $\/$
51		rexeq 2704	. . . . . . . . . . . . . . 15 $\/$ $\/$
52	51	imbi2d 230	. . . . . . . . . . . . . 14 $\/$ $\/$
53	52	ralbidv 2507	. . . . . . . . . . . . 13 $\/$ $\/$
54	50, 53	anbi12d 473	. . . . . . . . . . . 12 $\/$ $/\$ $\/$ $/\$ $\/$
55	54	rexbidv 2508	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $/\$ $\/$
56	49, 55	imbi12d 234	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
57		sup3exmid.ex	. . . . . . . . . 10 $/\$ $/\$ $/\$
58	43, 56, 57	vtocl 2829	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
59	15, 26, 40, 58	mp3an 1350	. . . . . . . 8 $\/$ $/\$ $\/$
60	59	a1i 9	. . . . . . 7 $\/$ $/\$ $\/$
61	5, 60	supclti 7112	. . . . . 6 $\/$
62	61	mptru 1382	. . . . 5 $\/$
63		axltwlin 8153	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
64	2, 3, 62, 63	mp3an 1350	. . . 4 $\/$ $\/$ $\/$
65	1, 64	ax-mp 5	. . 3 $\/$ $\/$ $\/$
66	5, 60	suplubti 7114	. . . . . . . 8 $/\$ $\/$ $\/$
67	66	mptru 1382	. . . . . . 7 $/\$ $\/$ $\/$
68	2, 67	mpan 424	. . . . . 6 $\/$ $\/$
69		df-rex 2491	. . . . . 6 $\/$ $\/$ $/\$
70	68, 69	sylib 122	. . . . 5 $\/$ $\/$ $/\$
71		eqeq1 2213	. . . . . . . . 9
72	71	orbi1d 793	. . . . . . . 8 $\/$ $\/$
73	72	elrab 2931	. . . . . . 7 $\/$ $/\$ $\/$
74		simpr 110	. . . . . . . . . 10 $/\$ $\/$ $/\$
75	74	gt0ne0d 8598	. . . . . . . . 9 $/\$ $\/$ $/\$
76	75	neneqd 2398	. . . . . . . 8 $/\$ $\/$ $/\$
77		simplr 528	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
78		orel1 727	. . . . . . . 8 $\/$
79	76, 77, 78	sylc 62	. . . . . . 7 $/\$ $\/$ $/\$
80	73, 79	sylanb 284	. . . . . 6 $\/$ $/\$
81	80	exlimiv 1622	. . . . 5 $\/$ $/\$
82	70, 81	syl 14	. . . 4 $\/$
83	3	ltnri 8178	. . . . . 6
84		iba 300	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
85	84	olcs 738	. . . . . . . . . . 11 $/\$ $\/$
86	73, 85	bitr4id 199	. . . . . . . . . 10 $\/$
87	86	eqrdv 2204	. . . . . . . . 9 $\/$
88	87	supeq1d 7101	. . . . . . . 8 $\/$
89	3	a1i 9	. . . . . . . . . 10
90	3	elexi 2786	. . . . . . . . . . . 12
91	90	prid2 3742	. . . . . . . . . . 11
92	91	a1i 9	. . . . . . . . . 10
93		elpri 3658	. . . . . . . . . . . 12 $\/$
94	2, 3	lenlti 8186	. . . . . . . . . . . . . . 15
95	29, 94	mpbi 145	. . . . . . . . . . . . . 14
96		breq2 4052	. . . . . . . . . . . . . 14
97	95, 96	mtbiri 677	. . . . . . . . . . . . 13
98		breq2 4052	. . . . . . . . . . . . . 14
99	83, 98	mtbiri 677	. . . . . . . . . . . . 13
100	97, 99	jaoi 718	. . . . . . . . . . . 12 $\/$
101	93, 100	syl 14	. . . . . . . . . . 11
102	101	adantl 277	. . . . . . . . . 10 $/\$
103	5, 89, 92, 102	supmaxti 7118	. . . . . . . . 9
104	103	mptru 1382	. . . . . . . 8
105	88, 104	eqtrdi 2255	. . . . . . 7 $\/$
106	105	breq1d 4058	. . . . . 6 $\/$
107	83, 106	mtbiri 677	. . . . 5 $\/$
108	107	con2i 628	. . . 4 $\/$
109	82, 108	orim12i 761	. . 3 $\/$ $\/$ $\/$ $\/$
110	65, 109	ax-mp 5	. 2 $\/$
111		df-dc 837	. 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 710 DECID wdc 836 $/\$ w3a 981

wceq 1373

wtru 1374

wex 1516

wcel 2177

wral 2485

wrex 2486

crab 2489

cvv 2773

wss 3168

cpr 3636 class class class wbr 4048

csup 7096

cr 7937

cc0 7938

c1 7939

clt 8120

cle 8121

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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4167 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-cnex 8029 ax-resscn 8030 ax-1re 8032 ax-addrcl 8035 ax-0lt1 8044 ax-rnegex 8047 ax-pre-ltirr 8050 ax-pre-ltwlin 8051 ax-pre-lttrn 8052 ax-pre-apti 8053

This theorem depends on definitions: df-bi 117 df-dc 837 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3001 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-pw 3620 df-sn 3641 df-pr 3642 df-op 3644 df-uni 3854 df-br 4049 df-opab 4111 df-xp 4686 df-cnv 4688 df-iota 5238 df-riota 5909 df-sup 7098 df-pnf 8122 df-mnf 8123 df-xr 8124 df-ltxr 8125 df-le 8126

This theorem is referenced by: (None)

W3C validator