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 8259

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 8290. (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 533	. . 3 $/\$ $/\$ $/\$ $\/$
2		eleq1w 2299	. . . 4
3	2	cbvexv 1974	. . 3
4	1, 3	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$
5		simplll 539	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6		simpr 110	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
7		simplrl 541	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
8		breq2 4129	. . . . . . . 8
9	8	ralbidv 2550	. . . . . . 7
10	9	cbvrexv 2787	. . . . . 6
11		breq1 4128	. . . . . . . 8
12	11	cbvralv 2786	. . . . . . 7
13	12	rexbii 2557	. . . . . 6
14	10, 13	bitri 184	. . . . 5
15	7, 14	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
16		simplrr 542	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
17		breq1 4128	. . . . . . . 8
18		breq1 4128	. . . . . . . . . 10
19	18	rexbidv 2551	. . . . . . . . 9
20	19	orbi1d 803	. . . . . . . 8 $\/$ $\/$
21	17, 20	imbi12d 234	. . . . . . 7 $\/$ $\/$
22		breq2 4129	. . . . . . . 8
23		breq2 4129	. . . . . . . . . 10
24	23	ralbidv 2550	. . . . . . . . 9
25	24	orbi2d 802	. . . . . . . 8 $\/$ $\/$
26	22, 25	imbi12d 234	. . . . . . 7 $\/$ $\/$
27	21, 26	cbvral2v 2799	. . . . . 6 $\/$ $\/$
28		breq2 4129	. . . . . . . . . 10
29	28	cbvrexv 2787	. . . . . . . . 9
30		breq1 4128	. . . . . . . . . 10
31	30	cbvralv 2786	. . . . . . . . 9
32	29, 31	orbi12i 776	. . . . . . . 8 $\/$ $\/$
33	32	imbi2i 226	. . . . . . 7 $\/$ $\/$
34	33	2ralbii 2558	. . . . . 6 $\/$ $\/$
35	27, 34	bitri 184	. . . . 5 $\/$ $\/$
36	16, 35	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
37		eqid 2238	. . . 4
38	5, 6, 15, 36, 37	axpre-suploclemres 8258	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
39	17	notbid 677	. . . . . . . 8
40	39	ralbidv 2550	. . . . . . 7
41	8	imbi1d 231	. . . . . . . 8
42	41	ralbidv 2550	. . . . . . 7
43	40, 42	anbi12d 477	. . . . . 6 $/\$ $/\$
44	43	cbvrexv 2787	. . . . 5 $/\$ $/\$
45	22	notbid 677	. . . . . . . 8
46	45	cbvralv 2786	. . . . . . 7
47		breq1 4128	. . . . . . . . . 10
48	47	rexbidv 2551	. . . . . . . . 9
49	11, 48	imbi12d 234	. . . . . . . 8
50	49	cbvralv 2786	. . . . . . 7
51	46, 50	anbi12i 464	. . . . . 6 $/\$ $/\$
52	51	rexbii 2557	. . . . 5 $/\$ $/\$
53	44, 52	bitri 184	. . . 4 $/\$ $/\$
54		breq2 4129	. . . . . . . . 9
55	54	cbvrexv 2787	. . . . . . . 8
56	55	imbi2i 226	. . . . . . 7
57	56	ralbii 2556	. . . . . 6
58	57	anbi2i 461	. . . . 5 $/\$ $/\$
59	58	rexbii 2557	. . . 4 $/\$ $/\$
60	53, 59	bitri 184	. . 3 $/\$ $/\$
61	38, 60	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	4, 61	exlimddv 1954	1 $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wex 1545

wcel 2209

wral 2528

wrex 2529

crab 2532

wss 3220

cop 3708 class class class wbr 4125

cnr 7654

c0r 7655

cr 8168

cltrr 8173

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-eprel 4429 df-id 4433 df-po 4436 df-iso 4437 df-iord 4506 df-on 4508 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-ov 6078 df-oprab 6079 df-mpo 6080 df-1st 6364 df-2nd 6365 df-recs 6566 df-irdg 6631 df-1o 6677 df-2o 6678 df-oadd 6681 df-omul 6682 df-er 6797 df-ec 6799 df-qs 6803 df-ni 7661 df-pli 7662 df-mi 7663 df-lti 7664 df-plpq 7701 df-mpq 7702 df-enq 7704 df-nqqs 7705 df-plqqs 7706 df-mqqs 7707 df-1nqqs 7708 df-rq 7709 df-ltnqqs 7710 df-enq0 7781 df-nq0 7782 df-0nq0 7783 df-plq0 7784 df-mq0 7785 df-inp 7823 df-i1p 7824 df-iplp 7825 df-imp 7826 df-iltp 7827 df-enr 8083 df-nr 8084 df-plr 8085 df-mr 8086 df-ltr 8087 df-0r 8088 df-1r 8089 df-m1r 8090 df-r 8179 df-lt 8182

This theorem is referenced by: (None)

W3C validator