sup3exmid - Intuitionistic Logic Explorer

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

Theorem sup3exmid 8715

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 7889	. . . 4
2		0re 7766	. . . . 5
3		1re 7765	. . . . 5
4		lttri3 7844	. . . . . . . 8 $/\$ $/\$
5	4	adantl 275	. . . . . . 7 $/\$ $/\$ $/\$
6		elrabi 2837	. . . . . . . . . . . 12 $\/$
7		elpri 3550	. . . . . . . . . . . 12 $\/$
8	6, 7	syl 14	. . . . . . . . . . 11 $\/$ $\/$
9		eleq1 2202	. . . . . . . . . . . . 13
10	2, 9	mpbiri 167	. . . . . . . . . . . 12
11		eleq1 2202	. . . . . . . . . . . . 13
12	3, 11	mpbiri 167	. . . . . . . . . . . 12
13	10, 12	jaoi 705	. . . . . . . . . . 11 $\/$
14	8, 13	syl 14	. . . . . . . . . 10 $\/$
15	14	ssriv 3101	. . . . . . . . 9 $\/$
16		eqid 2139	. . . . . . . . . . . 12
17	16	orci 720	. . . . . . . . . . 11 $\/$
18	2	elexi 2698	. . . . . . . . . . . . 13
19	18	prid1 3629	. . . . . . . . . . . 12
20		eqeq1 2146	. . . . . . . . . . . . . 14
21	20	orbi1d 780	. . . . . . . . . . . . 13 $\/$ $\/$
22	21	elrab3 2841	. . . . . . . . . . . 12 $\/$ $\/$
23	19, 22	ax-mp 5	. . . . . . . . . . 11 $\/$ $\/$
24	17, 23	mpbir 145	. . . . . . . . . 10 $\/$
25		elex2 2702	. . . . . . . . . 10 $\/$ $\/$
26	24, 25	ax-mp 5	. . . . . . . . 9 $\/$
27		elrabi 2837	. . . . . . . . . . . 12 $\/$
28		elpri 3550	. . . . . . . . . . . . 13 $\/$
29		0le1 8243	. . . . . . . . . . . . . . 15
30		breq1 3932	. . . . . . . . . . . . . . 15
31	29, 30	mpbiri 167	. . . . . . . . . . . . . 14
32	3	eqlei2 7858	. . . . . . . . . . . . . 14
33	31, 32	jaoi 705	. . . . . . . . . . . . 13 $\/$
34	28, 33	syl 14	. . . . . . . . . . . 12
35	27, 34	syl 14	. . . . . . . . . . 11 $\/$
36	35	rgen 2485	. . . . . . . . . 10 $\/$
37		breq2 3933	. . . . . . . . . . . 12
38	37	ralbidv 2437	. . . . . . . . . . 11 $\/$ $\/$
39	38	rspcev 2789	. . . . . . . . . 10 $/\$ $\/$ $\/$
40	3, 36, 39	mp2an 422	. . . . . . . . 9 $\/$
41		prexg 4133	. . . . . . . . . . . 12 $/\$
42	2, 3, 41	mp2an 422	. . . . . . . . . . 11
43	42	rabex 4072	. . . . . . . . . 10 $\/$
44		sseq1 3120	. . . . . . . . . . . 12 $\/$ $\/$
45		eleq2 2203	. . . . . . . . . . . . 13 $\/$ $\/$
46	45	exbidv 1797	. . . . . . . . . . . 12 $\/$ $\/$
47		raleq 2626	. . . . . . . . . . . . 13 $\/$ $\/$
48	47	rexbidv 2438	. . . . . . . . . . . 12 $\/$ $\/$
49	44, 46, 48	3anbi123d 1290	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
50		raleq 2626	. . . . . . . . . . . . 13 $\/$ $\/$
51		rexeq 2627	. . . . . . . . . . . . . . 15 $\/$ $\/$
52	51	imbi2d 229	. . . . . . . . . . . . . 14 $\/$ $\/$
53	52	ralbidv 2437	. . . . . . . . . . . . 13 $\/$ $\/$
54	50, 53	anbi12d 464	. . . . . . . . . . . 12 $\/$ $/\$ $\/$ $/\$ $\/$
55	54	rexbidv 2438	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $/\$ $\/$
56	49, 55	imbi12d 233	. . . . . . . . . 10 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
57		sup3exmid.ex	. . . . . . . . . 10 $/\$ $/\$ $/\$
58	43, 56, 57	vtocl 2740	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
59	15, 26, 40, 58	mp3an 1315	. . . . . . . 8 $\/$ $/\$ $\/$
60	59	a1i 9	. . . . . . 7 $\/$ $/\$ $\/$
61	5, 60	supclti 6885	. . . . . 6 $\/$
62	61	mptru 1340	. . . . 5 $\/$
63		axltwlin 7832	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$ $\/$
64	2, 3, 62, 63	mp3an 1315	. . . 4 $\/$ $\/$ $\/$
65	1, 64	ax-mp 5	. . 3 $\/$ $\/$ $\/$
66	5, 60	suplubti 6887	. . . . . . . 8 $/\$ $\/$ $\/$
67	66	mptru 1340	. . . . . . 7 $/\$ $\/$ $\/$
68	2, 67	mpan 420	. . . . . 6 $\/$ $\/$
69		df-rex 2422	. . . . . 6 $\/$ $\/$ $/\$
70	68, 69	sylib 121	. . . . 5 $\/$ $\/$ $/\$
71		eqeq1 2146	. . . . . . . . 9
72	71	orbi1d 780	. . . . . . . 8 $\/$ $\/$
73	72	elrab 2840	. . . . . . 7 $\/$ $/\$ $\/$
74		simpr 109	. . . . . . . . . 10 $/\$ $\/$ $/\$
75	74	gt0ne0d 8274	. . . . . . . . 9 $/\$ $\/$ $/\$
76	75	neneqd 2329	. . . . . . . 8 $/\$ $\/$ $/\$
77		simplr 519	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
78		orel1 714	. . . . . . . 8 $\/$
79	76, 77, 78	sylc 62	. . . . . . 7 $/\$ $\/$ $/\$
80	73, 79	sylanb 282	. . . . . 6 $\/$ $/\$
81	80	exlimiv 1577	. . . . 5 $\/$ $/\$
82	70, 81	syl 14	. . . 4 $\/$
83	3	ltnri 7856	. . . . . 6
84		iba 298	. . . . . . . . . . . 12 $\/$ $/\$ $\/$
85	84	olcs 725	. . . . . . . . . . 11 $/\$ $\/$
86	85, 73	syl6rbbr 198	. . . . . . . . . 10 $\/$
87	86	eqrdv 2137	. . . . . . . . 9 $\/$
88	87	supeq1d 6874	. . . . . . . 8 $\/$
89	3	a1i 9	. . . . . . . . . 10
90	3	elexi 2698	. . . . . . . . . . . 12
91	90	prid2 3630	. . . . . . . . . . 11
92	91	a1i 9	. . . . . . . . . 10
93		elpri 3550	. . . . . . . . . . . 12 $\/$
94	2, 3	lenlti 7864	. . . . . . . . . . . . . . 15
95	29, 94	mpbi 144	. . . . . . . . . . . . . 14
96		breq2 3933	. . . . . . . . . . . . . 14
97	95, 96	mtbiri 664	. . . . . . . . . . . . 13
98		breq2 3933	. . . . . . . . . . . . . 14
99	83, 98	mtbiri 664	. . . . . . . . . . . . 13
100	97, 99	jaoi 705	. . . . . . . . . . . 12 $\/$
101	93, 100	syl 14	. . . . . . . . . . 11
102	101	adantl 275	. . . . . . . . . 10 $/\$
103	5, 89, 92, 102	supmaxti 6891	. . . . . . . . 9
104	103	mptru 1340	. . . . . . . 8
105	88, 104	syl6eq 2188	. . . . . . 7 $\/$
106	105	breq1d 3939	. . . . . 6 $\/$
107	83, 106	mtbiri 664	. . . . 5 $\/$
108	107	con2i 616	. . . 4 $\/$
109	82, 108	orim12i 748	. . 3 $\/$ $\/$ $\/$ $\/$
110	65, 109	ax-mp 5	. 2 $\/$
111		df-dc 820	. 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 697 DECID wdc 819 $/\$ w3a 962

wceq 1331

wtru 1332

wex 1468

wcel 1480

wral 2416

wrex 2417

crab 2420

cvv 2686

wss 3071

cpr 3528 class class class wbr 3929

csup 6869

cr 7619

cc0 7620

c1 7621

clt 7800

cle 7801

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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-cnex 7711 ax-resscn 7712 ax-1re 7714 ax-addrcl 7717 ax-0lt1 7726 ax-rnegex 7729 ax-pre-ltirr 7732 ax-pre-ltwlin 7733 ax-pre-lttrn 7734 ax-pre-apti 7735

This theorem depends on definitions: df-bi 116 df-dc 820 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rmo 2424 df-rab 2425 df-v 2688 df-sbc 2910 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-br 3930 df-opab 3990 df-xp 4545 df-cnv 4547 df-iota 5088 df-riota 5730 df-sup 6871 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-le 7806

This theorem is referenced by: (None)

W3C validator