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 8121

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 8152. (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 2292	. . . 4
3	2	cbvexv 1967	. . 3
4	1, 3	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$
5		simplll 535	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6		simpr 110	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
7		simplrl 537	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
8		breq2 4092	. . . . . . . 8
9	8	ralbidv 2532	. . . . . . 7
10	9	cbvrexv 2768	. . . . . 6
11		breq1 4091	. . . . . . . 8
12	11	cbvralv 2767	. . . . . . 7
13	12	rexbii 2539	. . . . . 6
14	10, 13	bitri 184	. . . . 5
15	7, 14	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
16		simplrr 538	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
17		breq1 4091	. . . . . . . 8
18		breq1 4091	. . . . . . . . . 10
19	18	rexbidv 2533	. . . . . . . . 9
20	19	orbi1d 798	. . . . . . . 8 $\/$ $\/$
21	17, 20	imbi12d 234	. . . . . . 7 $\/$ $\/$
22		breq2 4092	. . . . . . . 8
23		breq2 4092	. . . . . . . . . 10
24	23	ralbidv 2532	. . . . . . . . 9
25	24	orbi2d 797	. . . . . . . 8 $\/$ $\/$
26	22, 25	imbi12d 234	. . . . . . 7 $\/$ $\/$
27	21, 26	cbvral2v 2780	. . . . . 6 $\/$ $\/$
28		breq2 4092	. . . . . . . . . 10
29	28	cbvrexv 2768	. . . . . . . . 9
30		breq1 4091	. . . . . . . . . 10
31	30	cbvralv 2767	. . . . . . . . 9
32	29, 31	orbi12i 771	. . . . . . . 8 $\/$ $\/$
33	32	imbi2i 226	. . . . . . 7 $\/$ $\/$
34	33	2ralbii 2540	. . . . . 6 $\/$ $\/$
35	27, 34	bitri 184	. . . . 5 $\/$ $\/$
36	16, 35	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
37		eqid 2231	. . . 4
38	5, 6, 15, 36, 37	axpre-suploclemres 8120	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
39	17	notbid 673	. . . . . . . 8
40	39	ralbidv 2532	. . . . . . 7
41	8	imbi1d 231	. . . . . . . 8
42	41	ralbidv 2532	. . . . . . 7
43	40, 42	anbi12d 473	. . . . . 6 $/\$ $/\$
44	43	cbvrexv 2768	. . . . 5 $/\$ $/\$
45	22	notbid 673	. . . . . . . 8
46	45	cbvralv 2767	. . . . . . 7
47		breq1 4091	. . . . . . . . . 10
48	47	rexbidv 2533	. . . . . . . . 9
49	11, 48	imbi12d 234	. . . . . . . 8
50	49	cbvralv 2767	. . . . . . 7
51	46, 50	anbi12i 460	. . . . . 6 $/\$ $/\$
52	51	rexbii 2539	. . . . 5 $/\$ $/\$
53	44, 52	bitri 184	. . . 4 $/\$ $/\$
54		breq2 4092	. . . . . . . . 9
55	54	cbvrexv 2768	. . . . . . . 8
56	55	imbi2i 226	. . . . . . 7
57	56	ralbii 2538	. . . . . 6
58	57	anbi2i 457	. . . . 5 $/\$ $/\$
59	58	rexbii 2539	. . . 4 $/\$ $/\$
60	53, 59	bitri 184	. . 3 $/\$ $/\$
61	38, 60	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	4, 61	exlimddv 1947	1 $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wex 1540

wcel 2202

wral 2510

wrex 2511

crab 2514

wss 3200

cop 3672 class class class wbr 4088

cnr 7516

c0r 7517

cr 8030

cltrr 8035

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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-ral 2515 df-rex 2516 df-reu 2517 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-eprel 4386 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-irdg 6535 df-1o 6581 df-2o 6582 df-oadd 6585 df-omul 6586 df-er 6701 df-ec 6703 df-qs 6707 df-ni 7523 df-pli 7524 df-mi 7525 df-lti 7526 df-plpq 7563 df-mpq 7564 df-enq 7566 df-nqqs 7567 df-plqqs 7568 df-mqqs 7569 df-1nqqs 7570 df-rq 7571 df-ltnqqs 7572 df-enq0 7643 df-nq0 7644 df-0nq0 7645 df-plq0 7646 df-mq0 7647 df-inp 7685 df-i1p 7686 df-iplp 7687 df-imp 7688 df-iltp 7689 df-enr 7945 df-nr 7946 df-plr 7947 df-mr 7948 df-ltr 7949 df-0r 7950 df-1r 7951 df-m1r 7952 df-r 8041 df-lt 8044

This theorem is referenced by: (None)

W3C validator