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 7918

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 7949. (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 528	. . 3 $/\$ $/\$ $/\$ $\/$
2		eleq1w 2249	. . . 4
3	2	cbvexv 1929	. . 3
4	1, 3	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$
5		simplll 533	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6		simpr 110	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
7		simplrl 535	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
8		breq2 4021	. . . . . . . 8
9	8	ralbidv 2489	. . . . . . 7
10	9	cbvrexv 2718	. . . . . 6
11		breq1 4020	. . . . . . . 8
12	11	cbvralv 2717	. . . . . . 7
13	12	rexbii 2496	. . . . . 6
14	10, 13	bitri 184	. . . . 5
15	7, 14	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
16		simplrr 536	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
17		breq1 4020	. . . . . . . 8
18		breq1 4020	. . . . . . . . . 10
19	18	rexbidv 2490	. . . . . . . . 9
20	19	orbi1d 792	. . . . . . . 8 $\/$ $\/$
21	17, 20	imbi12d 234	. . . . . . 7 $\/$ $\/$
22		breq2 4021	. . . . . . . 8
23		breq2 4021	. . . . . . . . . 10
24	23	ralbidv 2489	. . . . . . . . 9
25	24	orbi2d 791	. . . . . . . 8 $\/$ $\/$
26	22, 25	imbi12d 234	. . . . . . 7 $\/$ $\/$
27	21, 26	cbvral2v 2730	. . . . . 6 $\/$ $\/$
28		breq2 4021	. . . . . . . . . 10
29	28	cbvrexv 2718	. . . . . . . . 9
30		breq1 4020	. . . . . . . . . 10
31	30	cbvralv 2717	. . . . . . . . 9
32	29, 31	orbi12i 765	. . . . . . . 8 $\/$ $\/$
33	32	imbi2i 226	. . . . . . 7 $\/$ $\/$
34	33	2ralbii 2497	. . . . . 6 $\/$ $\/$
35	27, 34	bitri 184	. . . . 5 $\/$ $\/$
36	16, 35	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
37		eqid 2188	. . . 4
38	5, 6, 15, 36, 37	axpre-suploclemres 7917	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
39	17	notbid 668	. . . . . . . 8
40	39	ralbidv 2489	. . . . . . 7
41	8	imbi1d 231	. . . . . . . 8
42	41	ralbidv 2489	. . . . . . 7
43	40, 42	anbi12d 473	. . . . . 6 $/\$ $/\$
44	43	cbvrexv 2718	. . . . 5 $/\$ $/\$
45	22	notbid 668	. . . . . . . 8
46	45	cbvralv 2717	. . . . . . 7
47		breq1 4020	. . . . . . . . . 10
48	47	rexbidv 2490	. . . . . . . . 9
49	11, 48	imbi12d 234	. . . . . . . 8
50	49	cbvralv 2717	. . . . . . 7
51	46, 50	anbi12i 460	. . . . . 6 $/\$ $/\$
52	51	rexbii 2496	. . . . 5 $/\$ $/\$
53	44, 52	bitri 184	. . . 4 $/\$ $/\$
54		breq2 4021	. . . . . . . . 9
55	54	cbvrexv 2718	. . . . . . . 8
56	55	imbi2i 226	. . . . . . 7
57	56	ralbii 2495	. . . . . 6
58	57	anbi2i 457	. . . . 5 $/\$ $/\$
59	58	rexbii 2496	. . . 4 $/\$ $/\$
60	53, 59	bitri 184	. . 3 $/\$ $/\$
61	38, 60	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	4, 61	exlimddv 1909	1 $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 709

wex 1502

wcel 2159

wral 2467

wrex 2468

crab 2471

wss 3143

cop 3609 class class class wbr 4017

cnr 7313

c0r 7314

cr 7827

cltrr 7832

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 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2161 ax-14 2162 ax-ext 2170 ax-coll 4132 ax-sep 4135 ax-nul 4143 ax-pow 4188 ax-pr 4223 ax-un 4447 ax-setind 4550 ax-iinf 4601

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2040 df-mo 2041 df-clab 2175 df-cleq 2181 df-clel 2184 df-nfc 2320 df-ne 2360 df-ral 2472 df-rex 2473 df-reu 2474 df-rab 2476 df-v 2753 df-sbc 2977 df-csb 3072 df-dif 3145 df-un 3147 df-in 3149 df-ss 3156 df-nul 3437 df-pw 3591 df-sn 3612 df-pr 3613 df-op 3615 df-uni 3824 df-int 3859 df-iun 3902 df-br 4018 df-opab 4079 df-mpt 4080 df-tr 4116 df-eprel 4303 df-id 4307 df-po 4310 df-iso 4311 df-iord 4380 df-on 4382 df-suc 4385 df-iom 4604 df-xp 4646 df-rel 4647 df-cnv 4648 df-co 4649 df-dm 4650 df-rn 4651 df-res 4652 df-ima 4653 df-iota 5192 df-fun 5232 df-fn 5233 df-f 5234 df-f1 5235 df-fo 5236 df-f1o 5237 df-fv 5238 df-ov 5893 df-oprab 5894 df-mpo 5895 df-1st 6158 df-2nd 6159 df-recs 6323 df-irdg 6388 df-1o 6434 df-2o 6435 df-oadd 6438 df-omul 6439 df-er 6552 df-ec 6554 df-qs 6558 df-ni 7320 df-pli 7321 df-mi 7322 df-lti 7323 df-plpq 7360 df-mpq 7361 df-enq 7363 df-nqqs 7364 df-plqqs 7365 df-mqqs 7366 df-1nqqs 7367 df-rq 7368 df-ltnqqs 7369 df-enq0 7440 df-nq0 7441 df-0nq0 7442 df-plq0 7443 df-mq0 7444 df-inp 7482 df-i1p 7483 df-iplp 7484 df-imp 7485 df-iltp 7486 df-enr 7742 df-nr 7743 df-plr 7744 df-mr 7745 df-ltr 7746 df-0r 7747 df-1r 7748 df-m1r 7749 df-r 7838 df-lt 7841

This theorem is referenced by: (None)

W3C validator