Theorem axpre-suploc 8269

Description: An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given x < y, either there is an element of the set greater than x, or y is an upper bound.

This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 8300. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)

Assertion

Ref	Expression
axpre-suploc	|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )

Distinct variable group:   x, A, y, z

Proof of Theorem axpre-suploc

Dummy variables a b c d w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 533	. . 3 |- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. x x e. A )
2		eleq1w 2299	. . . 4 |- ( x = d -> ( x e. A <-> d e. A ) )
3	2	cbvexv 1974	. . 3 |- ( E. x x e. A <-> E. d d e. A )
4	1, 3	sylib 122	. 2 |- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. d d e. A )
5		simplll 539	. . . 4 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> A C_ RR )
6		simpr 110	. . . 4 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> d e. A )
7		simplrl 541	. . . . 5 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> E. x e. RR A. y e. A y <RR x )
8		breq2 4134	. . . . . . . 8 |- ( a = x -> ( b <RR a <-> b <RR x ) )
9	8	ralbidv 2550	. . . . . . 7 |- ( a = x -> ( A. b e. A b <RR a <-> A. b e. A b <RR x ) )
10	9	cbvrexv 2787	. . . . . 6 |- ( E. a e. RR A. b e. A b <RR a <-> E. x e. RR A. b e. A b <RR x )
11		breq1 4133	. . . . . . . 8 |- ( b = y -> ( b <RR x <-> y <RR x ) )
12	11	cbvralv 2786	. . . . . . 7 |- ( A. b e. A b <RR x <-> A. y e. A y <RR x )
13	12	rexbii 2557	. . . . . 6 |- ( E. x e. RR A. b e. A b <RR x <-> E. x e. RR A. y e. A y <RR x )
14	10, 13	bitri 184	. . . . 5 |- ( E. a e. RR A. b e. A b <RR a <-> E. x e. RR A. y e. A y <RR x )
15	7, 14	sylibr 134	. . . 4 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> E. a e. RR A. b e. A b <RR a )
16		simplrr 542	. . . . 5 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) )
17		breq1 4133	. . . . . . . 8 |- ( a = x -> ( a <RR b <-> x <RR b ) )
18		breq1 4133	. . . . . . . . . 10 |- ( a = x -> ( a <RR c <-> x <RR c ) )
19	18	rexbidv 2551	. . . . . . . . 9 |- ( a = x -> ( E. c e. A a <RR c <-> E. c e. A x <RR c ) )
20	19	orbi1d 803	. . . . . . . 8 |- ( a = x -> ( ( E. c e. A a <RR c \/ A. c e. A c <RR b ) <-> ( E. c e. A x <RR c \/ A. c e. A c <RR b ) ) )
21	17, 20	imbi12d 234	. . . . . . 7 |- ( a = x -> ( ( a <RR b -> ( E. c e. A a <RR c \/ A. c e. A c <RR b ) ) <-> ( x <RR b -> ( E. c e. A x <RR c \/ A. c e. A c <RR b ) ) ) )
22		breq2 4134	. . . . . . . 8 |- ( b = y -> ( x <RR b <-> x <RR y ) )
23		breq2 4134	. . . . . . . . . 10 |- ( b = y -> ( c <RR b <-> c <RR y ) )
24	23	ralbidv 2550	. . . . . . . . 9 |- ( b = y -> ( A. c e. A c <RR b <-> A. c e. A c <RR y ) )
25	24	orbi2d 802	. . . . . . . 8 |- ( b = y -> ( ( E. c e. A x <RR c \/ A. c e. A c <RR b ) <-> ( E. c e. A x <RR c \/ A. c e. A c <RR y ) ) )
26	22, 25	imbi12d 234	. . . . . . 7 |- ( b = y -> ( ( x <RR b -> ( E. c e. A x <RR c \/ A. c e. A c <RR b ) ) <-> ( x <RR y -> ( E. c e. A x <RR c \/ A. c e. A c <RR y ) ) ) )
27	21, 26	cbvral2v 2799	. . . . . 6 |- ( A. a e. RR A. b e. RR ( a <RR b -> ( E. c e. A a <RR c \/ A. c e. A c <RR b ) ) <-> A. x e. RR A. y e. RR ( x <RR y -> ( E. c e. A x <RR c \/ A. c e. A c <RR y ) ) )
28		breq2 4134	. . . . . . . . . 10 |- ( c = z -> ( x <RR c <-> x <RR z ) )
29	28	cbvrexv 2787	. . . . . . . . 9 |- ( E. c e. A x <RR c <-> E. z e. A x <RR z )
30		breq1 4133	. . . . . . . . . 10 |- ( c = z -> ( c <RR y <-> z <RR y ) )
31	30	cbvralv 2786	. . . . . . . . 9 |- ( A. c e. A c <RR y <-> A. z e. A z <RR y )
32	29, 31	orbi12i 776	. . . . . . . 8 |- ( ( E. c e. A x <RR c \/ A. c e. A c <RR y ) <-> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) )
33	32	imbi2i 226	. . . . . . 7 |- ( ( x <RR y -> ( E. c e. A x <RR c \/ A. c e. A c <RR y ) ) <-> ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) )
34	33	2ralbii 2558	. . . . . 6 |- ( A. x e. RR A. y e. RR ( x <RR y -> ( E. c e. A x <RR c \/ A. c e. A c <RR y ) ) <-> A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) )
35	27, 34	bitri 184	. . . . 5 |- ( A. a e. RR A. b e. RR ( a <RR b -> ( E. c e. A a <RR c \/ A. c e. A c <RR b ) ) <-> A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) )
36	16, 35	sylibr 134	. . . 4 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> A. a e. RR A. b e. RR ( a <RR b -> ( E. c e. A a <RR c \/ A. c e. A c <RR b ) ) )
37		eqid 2238	. . . 4 |- { w e. R. | <. w , 0R >. e. A } = { w e. R. | <. w , 0R >. e. A }
38	5, 6, 15, 36, 37	axpre-suploclemres 8268	. . 3 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> E. a e. RR ( A. b e. A -. a <RR b /\ A. b e. RR ( b <RR a -> E. c e. A b <RR c ) ) )
39	17	notbid 677	. . . . . . . 8 |- ( a = x -> ( -. a <RR b <-> -. x <RR b ) )
40	39	ralbidv 2550	. . . . . . 7 |- ( a = x -> ( A. b e. A -. a <RR b <-> A. b e. A -. x <RR b ) )
41	8	imbi1d 231	. . . . . . . 8 |- ( a = x -> ( ( b <RR a -> E. c e. A b <RR c ) <-> ( b <RR x -> E. c e. A b <RR c ) ) )
42	41	ralbidv 2550	. . . . . . 7 |- ( a = x -> ( A. b e. RR ( b <RR a -> E. c e. A b <RR c ) <-> A. b e. RR ( b <RR x -> E. c e. A b <RR c ) ) )
43	40, 42	anbi12d 477	. . . . . 6 |- ( a = x -> ( ( A. b e. A -. a <RR b /\ A. b e. RR ( b <RR a -> E. c e. A b <RR c ) ) <-> ( A. b e. A -. x <RR b /\ A. b e. RR ( b <RR x -> E. c e. A b <RR c ) ) ) )
44	43	cbvrexv 2787	. . . . 5 |- ( E. a e. RR ( A. b e. A -. a <RR b /\ A. b e. RR ( b <RR a -> E. c e. A b <RR c ) ) <-> E. x e. RR ( A. b e. A -. x <RR b /\ A. b e. RR ( b <RR x -> E. c e. A b <RR c ) ) )
45	22	notbid 677	. . . . . . . 8 |- ( b = y -> ( -. x <RR b <-> -. x <RR y ) )
46	45	cbvralv 2786	. . . . . . 7 |- ( A. b e. A -. x <RR b <-> A. y e. A -. x <RR y )
47		breq1 4133	. . . . . . . . . 10 |- ( b = y -> ( b <RR c <-> y <RR c ) )
48	47	rexbidv 2551	. . . . . . . . 9 |- ( b = y -> ( E. c e. A b <RR c <-> E. c e. A y <RR c ) )
49	11, 48	imbi12d 234	. . . . . . . 8 |- ( b = y -> ( ( b <RR x -> E. c e. A b <RR c ) <-> ( y <RR x -> E. c e. A y <RR c ) ) )
50	49	cbvralv 2786	. . . . . . 7 |- ( A. b e. RR ( b <RR x -> E. c e. A b <RR c ) <-> A. y e. RR ( y <RR x -> E. c e. A y <RR c ) )
51	46, 50	anbi12i 464	. . . . . 6 |- ( ( A. b e. A -. x <RR b /\ A. b e. RR ( b <RR x -> E. c e. A b <RR c ) ) <-> ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. c e. A y <RR c ) ) )
52	51	rexbii 2557	. . . . 5 |- ( E. x e. RR ( A. b e. A -. x <RR b /\ A. b e. RR ( b <RR x -> E. c e. A b <RR c ) ) <-> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. c e. A y <RR c ) ) )
53	44, 52	bitri 184	. . . 4 |- ( E. a e. RR ( A. b e. A -. a <RR b /\ A. b e. RR ( b <RR a -> E. c e. A b <RR c ) ) <-> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. c e. A y <RR c ) ) )
54		breq2 4134	. . . . . . . . 9 |- ( c = z -> ( y <RR c <-> y <RR z ) )
55	54	cbvrexv 2787	. . . . . . . 8 |- ( E. c e. A y <RR c <-> E. z e. A y <RR z )
56	55	imbi2i 226	. . . . . . 7 |- ( ( y <RR x -> E. c e. A y <RR c ) <-> ( y <RR x -> E. z e. A y <RR z ) )
57	56	ralbii 2556	. . . . . 6 |- ( A. y e. RR ( y <RR x -> E. c e. A y <RR c ) <-> A. y e. RR ( y <RR x -> E. z e. A y <RR z ) )
58	57	anbi2i 461	. . . . 5 |- ( ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. c e. A y <RR c ) ) <-> ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
59	58	rexbii 2557	. . . 4 |- ( E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. c e. A y <RR c ) ) <-> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
60	53, 59	bitri 184	. . 3 |- ( E. a e. RR ( A. b e. A -. a <RR b /\ A. b e. RR ( b <RR a -> E. c e. A b <RR c ) ) <-> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
61	38, 60	sylib 122	. 2 |- ( ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) /\ d e. A ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
62	4, 61	exlimddv 1954	1 |- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 720   E.wex 1545   e. wcel 2209   A.wral 2528   E.wrex 2529   {crab 2532   C_ wss 3220   <.cop 3712   class class class wbr 4130   R.cnr 7664   0Rc0r 7665   RRcr 8178   <RR cltrr 8183

This proof depends on 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 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735

This proof 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 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-eprel 4434  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-1o 6687  df-2o 6688  df-oadd 6691  df-omul 6692  df-er 6807  df-ec 6809  df-qs 6813  df-ni 7671  df-pli 7672  df-mi 7673  df-lti 7674  df-plpq 7711  df-mpq 7712  df-enq 7714  df-nqqs 7715  df-plqqs 7716  df-mqqs 7717  df-1nqqs 7718  df-rq 7719  df-ltnqqs 7720  df-enq0 7791  df-nq0 7792  df-0nq0 7793  df-plq0 7794  df-mq0 7795  df-inp 7833  df-i1p 7834  df-iplp 7835  df-imp 7836  df-iltp 7837  df-enr 8093  df-nr 8094  df-plr 8095  df-mr 8096  df-ltr 8097  df-0r 8098  df-1r 8099  df-m1r 8100  df-r 8189  df-lt 8192

This theorem is used by: (None)