axpre-suploc - Intuitionistic Logic Explorer

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

Theorem axpre-suploc 7843

Description: An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given , either there is an element of the set greater than , or is an upper bound.

This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7874. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)

**Assertion**
Ref	Expression
axpre-suploc	$/\$ $/\$ $/\$ $\/$ $/\$

Distinct variable group:

Proof of Theorem axpre-suploc Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 520	. . 3 $/\$ $/\$ $/\$ $\/$
2		eleq1w 2227	. . . 4
3	2	cbvexv 1906	. . 3
4	1, 3	sylib 121	. 2 $/\$ $/\$ $/\$ $\/$
5		simplll 523	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6		simpr 109	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
7		simplrl 525	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
8		breq2 3986	. . . . . . . 8
9	8	ralbidv 2466	. . . . . . 7
10	9	cbvrexv 2693	. . . . . 6
11		breq1 3985	. . . . . . . 8
12	11	cbvralv 2692	. . . . . . 7
13	12	rexbii 2473	. . . . . 6
14	10, 13	bitri 183	. . . . 5
15	7, 14	sylibr 133	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
16		simplrr 526	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
17		breq1 3985	. . . . . . . 8
18		breq1 3985	. . . . . . . . . 10
19	18	rexbidv 2467	. . . . . . . . 9
20	19	orbi1d 781	. . . . . . . 8 $\/$ $\/$
21	17, 20	imbi12d 233	. . . . . . 7 $\/$ $\/$
22		breq2 3986	. . . . . . . 8
23		breq2 3986	. . . . . . . . . 10
24	23	ralbidv 2466	. . . . . . . . 9
25	24	orbi2d 780	. . . . . . . 8 $\/$ $\/$
26	22, 25	imbi12d 233	. . . . . . 7 $\/$ $\/$
27	21, 26	cbvral2v 2705	. . . . . 6 $\/$ $\/$
28		breq2 3986	. . . . . . . . . 10
29	28	cbvrexv 2693	. . . . . . . . 9
30		breq1 3985	. . . . . . . . . 10
31	30	cbvralv 2692	. . . . . . . . 9
32	29, 31	orbi12i 754	. . . . . . . 8 $\/$ $\/$
33	32	imbi2i 225	. . . . . . 7 $\/$ $\/$
34	33	2ralbii 2474	. . . . . 6 $\/$ $\/$
35	27, 34	bitri 183	. . . . 5 $\/$ $\/$
36	16, 35	sylibr 133	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
37		eqid 2165	. . . 4
38	5, 6, 15, 36, 37	axpre-suploclemres 7842	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
39	17	notbid 657	. . . . . . . 8
40	39	ralbidv 2466	. . . . . . 7
41	8	imbi1d 230	. . . . . . . 8
42	41	ralbidv 2466	. . . . . . 7
43	40, 42	anbi12d 465	. . . . . 6 $/\$ $/\$
44	43	cbvrexv 2693	. . . . 5 $/\$ $/\$
45	22	notbid 657	. . . . . . . 8
46	45	cbvralv 2692	. . . . . . 7
47		breq1 3985	. . . . . . . . . 10
48	47	rexbidv 2467	. . . . . . . . 9
49	11, 48	imbi12d 233	. . . . . . . 8
50	49	cbvralv 2692	. . . . . . 7
51	46, 50	anbi12i 456	. . . . . 6 $/\$ $/\$
52	51	rexbii 2473	. . . . 5 $/\$ $/\$
53	44, 52	bitri 183	. . . 4 $/\$ $/\$
54		breq2 3986	. . . . . . . . 9
55	54	cbvrexv 2693	. . . . . . . 8
56	55	imbi2i 225	. . . . . . 7
57	56	ralbii 2472	. . . . . 6
58	57	anbi2i 453	. . . . 5 $/\$ $/\$
59	58	rexbii 2473	. . . 4 $/\$ $/\$
60	53, 59	bitri 183	. . 3 $/\$ $/\$
61	38, 60	sylib 121	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	4, 61	exlimddv 1886	1 $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103 $\/$ wo 698

wex 1480

wcel 2136

wral 2444

wrex 2445

crab 2448

wss 3116

cop 3579 class class class wbr 3982

cnr 7238

c0r 7239

cr 7752

cltrr 7757

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 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-reu 2451 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-eprel 4267 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-1o 6384 df-2o 6385 df-oadd 6388 df-omul 6389 df-er 6501 df-ec 6503 df-qs 6507 df-ni 7245 df-pli 7246 df-mi 7247 df-lti 7248 df-plpq 7285 df-mpq 7286 df-enq 7288 df-nqqs 7289 df-plqqs 7290 df-mqqs 7291 df-1nqqs 7292 df-rq 7293 df-ltnqqs 7294 df-enq0 7365 df-nq0 7366 df-0nq0 7367 df-plq0 7368 df-mq0 7369 df-inp 7407 df-i1p 7408 df-iplp 7409 df-imp 7410 df-iltp 7411 df-enr 7667 df-nr 7668 df-plr 7669 df-mr 7670 df-ltr 7671 df-0r 7672 df-1r 7673 df-m1r 7674 df-r 7763 df-lt 7766

This theorem is referenced by: (None)

W3C validator