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 8112

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 8143. (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 2290	. . . 4
3	2	cbvexv 1965	. . 3
4	1, 3	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$
5		simplll 533	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6		simpr 110	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
7		simplrl 535	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
8		breq2 4090	. . . . . . . 8
9	8	ralbidv 2530	. . . . . . 7
10	9	cbvrexv 2766	. . . . . 6
11		breq1 4089	. . . . . . . 8
12	11	cbvralv 2765	. . . . . . 7
13	12	rexbii 2537	. . . . . 6
14	10, 13	bitri 184	. . . . 5
15	7, 14	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
16		simplrr 536	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
17		breq1 4089	. . . . . . . 8
18		breq1 4089	. . . . . . . . . 10
19	18	rexbidv 2531	. . . . . . . . 9
20	19	orbi1d 796	. . . . . . . 8 $\/$ $\/$
21	17, 20	imbi12d 234	. . . . . . 7 $\/$ $\/$
22		breq2 4090	. . . . . . . 8
23		breq2 4090	. . . . . . . . . 10
24	23	ralbidv 2530	. . . . . . . . 9
25	24	orbi2d 795	. . . . . . . 8 $\/$ $\/$
26	22, 25	imbi12d 234	. . . . . . 7 $\/$ $\/$
27	21, 26	cbvral2v 2778	. . . . . 6 $\/$ $\/$
28		breq2 4090	. . . . . . . . . 10
29	28	cbvrexv 2766	. . . . . . . . 9
30		breq1 4089	. . . . . . . . . 10
31	30	cbvralv 2765	. . . . . . . . 9
32	29, 31	orbi12i 769	. . . . . . . 8 $\/$ $\/$
33	32	imbi2i 226	. . . . . . 7 $\/$ $\/$
34	33	2ralbii 2538	. . . . . 6 $\/$ $\/$
35	27, 34	bitri 184	. . . . 5 $\/$ $\/$
36	16, 35	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
37		eqid 2229	. . . 4
38	5, 6, 15, 36, 37	axpre-suploclemres 8111	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
39	17	notbid 671	. . . . . . . 8
40	39	ralbidv 2530	. . . . . . 7
41	8	imbi1d 231	. . . . . . . 8
42	41	ralbidv 2530	. . . . . . 7
43	40, 42	anbi12d 473	. . . . . 6 $/\$ $/\$
44	43	cbvrexv 2766	. . . . 5 $/\$ $/\$
45	22	notbid 671	. . . . . . . 8
46	45	cbvralv 2765	. . . . . . 7
47		breq1 4089	. . . . . . . . . 10
48	47	rexbidv 2531	. . . . . . . . 9
49	11, 48	imbi12d 234	. . . . . . . 8
50	49	cbvralv 2765	. . . . . . 7
51	46, 50	anbi12i 460	. . . . . 6 $/\$ $/\$
52	51	rexbii 2537	. . . . 5 $/\$ $/\$
53	44, 52	bitri 184	. . . 4 $/\$ $/\$
54		breq2 4090	. . . . . . . . 9
55	54	cbvrexv 2766	. . . . . . . 8
56	55	imbi2i 226	. . . . . . 7
57	56	ralbii 2536	. . . . . 6
58	57	anbi2i 457	. . . . 5 $/\$ $/\$
59	58	rexbii 2537	. . . 4 $/\$ $/\$
60	53, 59	bitri 184	. . 3 $/\$ $/\$
61	38, 60	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	4, 61	exlimddv 1945	1 $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wex 1538

wcel 2200

wral 2508

wrex 2509

crab 2512

wss 3198

cop 3670 class class class wbr 4086

cnr 7507

c0r 7508

cr 8021

cltrr 8026

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-coll 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 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-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-eprel 4384 df-id 4388 df-po 4391 df-iso 4392 df-iord 4461 df-on 4463 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-ov 6016 df-oprab 6017 df-mpo 6018 df-1st 6298 df-2nd 6299 df-recs 6466 df-irdg 6531 df-1o 6577 df-2o 6578 df-oadd 6581 df-omul 6582 df-er 6697 df-ec 6699 df-qs 6703 df-ni 7514 df-pli 7515 df-mi 7516 df-lti 7517 df-plpq 7554 df-mpq 7555 df-enq 7557 df-nqqs 7558 df-plqqs 7559 df-mqqs 7560 df-1nqqs 7561 df-rq 7562 df-ltnqqs 7563 df-enq0 7634 df-nq0 7635 df-0nq0 7636 df-plq0 7637 df-mq0 7638 df-inp 7676 df-i1p 7677 df-iplp 7678 df-imp 7679 df-iltp 7680 df-enr 7936 df-nr 7937 df-plr 7938 df-mr 7939 df-ltr 7940 df-0r 7941 df-1r 7942 df-m1r 7943 df-r 8032 df-lt 8035

This theorem is referenced by: (None)

W3C validator