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 8219

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 8250. (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 529	. . 3 $/\$ $/\$ $/\$ $\/$
2		eleq1w 2295	. . . 4
3	2	cbvexv 1970	. . 3
4	1, 3	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$
5		simplll 535	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6		simpr 110	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
7		simplrl 537	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
8		breq2 4115	. . . . . . . 8
9	8	ralbidv 2544	. . . . . . 7
10	9	cbvrexv 2781	. . . . . 6
11		breq1 4114	. . . . . . . 8
12	11	cbvralv 2780	. . . . . . 7
13	12	rexbii 2551	. . . . . 6
14	10, 13	bitri 184	. . . . 5
15	7, 14	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
16		simplrr 538	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
17		breq1 4114	. . . . . . . 8
18		breq1 4114	. . . . . . . . . 10
19	18	rexbidv 2545	. . . . . . . . 9
20	19	orbi1d 799	. . . . . . . 8 $\/$ $\/$
21	17, 20	imbi12d 234	. . . . . . 7 $\/$ $\/$
22		breq2 4115	. . . . . . . 8
23		breq2 4115	. . . . . . . . . 10
24	23	ralbidv 2544	. . . . . . . . 9
25	24	orbi2d 798	. . . . . . . 8 $\/$ $\/$
26	22, 25	imbi12d 234	. . . . . . 7 $\/$ $\/$
27	21, 26	cbvral2v 2793	. . . . . 6 $\/$ $\/$
28		breq2 4115	. . . . . . . . . 10
29	28	cbvrexv 2781	. . . . . . . . 9
30		breq1 4114	. . . . . . . . . 10
31	30	cbvralv 2780	. . . . . . . . 9
32	29, 31	orbi12i 772	. . . . . . . 8 $\/$ $\/$
33	32	imbi2i 226	. . . . . . 7 $\/$ $\/$
34	33	2ralbii 2552	. . . . . 6 $\/$ $\/$
35	27, 34	bitri 184	. . . . 5 $\/$ $\/$
36	16, 35	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
37		eqid 2234	. . . 4
38	5, 6, 15, 36, 37	axpre-suploclemres 8218	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
39	17	notbid 673	. . . . . . . 8
40	39	ralbidv 2544	. . . . . . 7
41	8	imbi1d 231	. . . . . . . 8
42	41	ralbidv 2544	. . . . . . 7
43	40, 42	anbi12d 473	. . . . . 6 $/\$ $/\$
44	43	cbvrexv 2781	. . . . 5 $/\$ $/\$
45	22	notbid 673	. . . . . . . 8
46	45	cbvralv 2780	. . . . . . 7
47		breq1 4114	. . . . . . . . . 10
48	47	rexbidv 2545	. . . . . . . . 9
49	11, 48	imbi12d 234	. . . . . . . 8
50	49	cbvralv 2780	. . . . . . 7
51	46, 50	anbi12i 460	. . . . . 6 $/\$ $/\$
52	51	rexbii 2551	. . . . 5 $/\$ $/\$
53	44, 52	bitri 184	. . . 4 $/\$ $/\$
54		breq2 4115	. . . . . . . . 9
55	54	cbvrexv 2781	. . . . . . . 8
56	55	imbi2i 226	. . . . . . 7
57	56	ralbii 2550	. . . . . 6
58	57	anbi2i 457	. . . . 5 $/\$ $/\$
59	58	rexbii 2551	. . . 4 $/\$ $/\$
60	53, 59	bitri 184	. . 3 $/\$ $/\$
61	38, 60	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	4, 61	exlimddv 1950	1 $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wex 1541

wcel 2205

wral 2522

wrex 2523

crab 2526

wss 3213

cop 3694 class class class wbr 4111

cnr 7614

c0r 7615

cr 8128

cltrr 8133

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4227 ax-sep 4230 ax-nul 4238 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-iinf 4712

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-ral 2527 df-rex 2528 df-reu 2529 df-rab 2531 df-v 2817 df-sbc 3045 df-csb 3141 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-nul 3511 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-int 3952 df-iun 3995 df-br 4112 df-opab 4174 df-mpt 4175 df-tr 4211 df-eprel 4412 df-id 4416 df-po 4419 df-iso 4420 df-iord 4489 df-on 4491 df-suc 4494 df-iom 4715 df-xp 4757 df-rel 4758 df-cnv 4759 df-co 4760 df-dm 4761 df-rn 4762 df-res 4763 df-ima 4764 df-iota 5314 df-fun 5356 df-fn 5357 df-f 5358 df-f1 5359 df-fo 5360 df-f1o 5361 df-fv 5362 df-ov 6055 df-oprab 6056 df-mpo 6057 df-1st 6336 df-2nd 6337 df-recs 6538 df-irdg 6603 df-1o 6649 df-2o 6650 df-oadd 6653 df-omul 6654 df-er 6769 df-ec 6771 df-qs 6775 df-ni 7621 df-pli 7622 df-mi 7623 df-lti 7624 df-plpq 7661 df-mpq 7662 df-enq 7664 df-nqqs 7665 df-plqqs 7666 df-mqqs 7667 df-1nqqs 7668 df-rq 7669 df-ltnqqs 7670 df-enq0 7741 df-nq0 7742 df-0nq0 7743 df-plq0 7744 df-mq0 7745 df-inp 7783 df-i1p 7784 df-iplp 7785 df-imp 7786 df-iltp 7787 df-enr 8043 df-nr 8044 df-plr 8045 df-mr 8046 df-ltr 8047 df-0r 8048 df-1r 8049 df-m1r 8050 df-r 8139 df-lt 8142

This theorem is referenced by: (None)

W3C validator