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 7892

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 7923. (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 2238	. . . 4
3	2	cbvexv 1918	. . 3
4	1, 3	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$
5		simplll 533	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6		simpr 110	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
7		simplrl 535	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
8		breq2 4004	. . . . . . . 8
9	8	ralbidv 2477	. . . . . . 7
10	9	cbvrexv 2704	. . . . . 6
11		breq1 4003	. . . . . . . 8
12	11	cbvralv 2703	. . . . . . 7
13	12	rexbii 2484	. . . . . 6
14	10, 13	bitri 184	. . . . 5
15	7, 14	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
16		simplrr 536	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
17		breq1 4003	. . . . . . . 8
18		breq1 4003	. . . . . . . . . 10
19	18	rexbidv 2478	. . . . . . . . 9
20	19	orbi1d 791	. . . . . . . 8 $\/$ $\/$
21	17, 20	imbi12d 234	. . . . . . 7 $\/$ $\/$
22		breq2 4004	. . . . . . . 8
23		breq2 4004	. . . . . . . . . 10
24	23	ralbidv 2477	. . . . . . . . 9
25	24	orbi2d 790	. . . . . . . 8 $\/$ $\/$
26	22, 25	imbi12d 234	. . . . . . 7 $\/$ $\/$
27	21, 26	cbvral2v 2716	. . . . . 6 $\/$ $\/$
28		breq2 4004	. . . . . . . . . 10
29	28	cbvrexv 2704	. . . . . . . . 9
30		breq1 4003	. . . . . . . . . 10
31	30	cbvralv 2703	. . . . . . . . 9
32	29, 31	orbi12i 764	. . . . . . . 8 $\/$ $\/$
33	32	imbi2i 226	. . . . . . 7 $\/$ $\/$
34	33	2ralbii 2485	. . . . . 6 $\/$ $\/$
35	27, 34	bitri 184	. . . . 5 $\/$ $\/$
36	16, 35	sylibr 134	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
37		eqid 2177	. . . 4
38	5, 6, 15, 36, 37	axpre-suploclemres 7891	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
39	17	notbid 667	. . . . . . . 8
40	39	ralbidv 2477	. . . . . . 7
41	8	imbi1d 231	. . . . . . . 8
42	41	ralbidv 2477	. . . . . . 7
43	40, 42	anbi12d 473	. . . . . 6 $/\$ $/\$
44	43	cbvrexv 2704	. . . . 5 $/\$ $/\$
45	22	notbid 667	. . . . . . . 8
46	45	cbvralv 2703	. . . . . . 7
47		breq1 4003	. . . . . . . . . 10
48	47	rexbidv 2478	. . . . . . . . 9
49	11, 48	imbi12d 234	. . . . . . . 8
50	49	cbvralv 2703	. . . . . . 7
51	46, 50	anbi12i 460	. . . . . 6 $/\$ $/\$
52	51	rexbii 2484	. . . . 5 $/\$ $/\$
53	44, 52	bitri 184	. . . 4 $/\$ $/\$
54		breq2 4004	. . . . . . . . 9
55	54	cbvrexv 2704	. . . . . . . 8
56	55	imbi2i 226	. . . . . . 7
57	56	ralbii 2483	. . . . . 6
58	57	anbi2i 457	. . . . 5 $/\$ $/\$
59	58	rexbii 2484	. . . 4 $/\$ $/\$
60	53, 59	bitri 184	. . 3 $/\$ $/\$
61	38, 60	sylib 122	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	4, 61	exlimddv 1898	1 $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wex 1492

wcel 2148

wral 2455

wrex 2456

crab 2459

wss 3129

cop 3594 class class class wbr 4000

cnr 7287

c0r 7288

cr 7801

cltrr 7806

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-reu 2462 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-eprel 4286 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-recs 6300 df-irdg 6365 df-1o 6411 df-2o 6412 df-oadd 6415 df-omul 6416 df-er 6529 df-ec 6531 df-qs 6535 df-ni 7294 df-pli 7295 df-mi 7296 df-lti 7297 df-plpq 7334 df-mpq 7335 df-enq 7337 df-nqqs 7338 df-plqqs 7339 df-mqqs 7340 df-1nqqs 7341 df-rq 7342 df-ltnqqs 7343 df-enq0 7414 df-nq0 7415 df-0nq0 7416 df-plq0 7417 df-mq0 7418 df-inp 7456 df-i1p 7457 df-iplp 7458 df-imp 7459 df-iltp 7460 df-enr 7716 df-nr 7717 df-plr 7718 df-mr 7719 df-ltr 7720 df-0r 7721 df-1r 7722 df-m1r 7723 df-r 7812 df-lt 7815

This theorem is referenced by: (None)

W3C validator