Axiom ax-pre-suploc 8017

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.

Although this and ax-caucvg 8016 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 8016.

(Contributed by Jim Kingdon, 23-Jan-2024.)

Assertion

Ref	Expression
ax-pre-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

Detailed syntax breakdown of Axiom ax-pre-suploc

Step	Hyp	Ref	Expression
1		cA	. . . . 5 class A
2		cr 7895	. . . . 5 class RR
3	1, 2	wss 3157	. . . 4 wff A C_ RR
4		vx	. . . . . . 7 setvar x
5	4	cv 1363	. . . . . 6 class x
6	5, 1	wcel 2167	. . . . 5 wff x e. A
7	6, 4	wex 1506	. . . 4 wff E. x x e. A
8	3, 7	wa 104	. . 3 wff ( A C_ RR /\ E. x x e. A )
9		vy	. . . . . . . 8 setvar y
10	9	cv 1363	. . . . . . 7 class y
11		cltrr 7900	. . . . . . 7 class <RR
12	10, 5, 11	wbr 4034	. . . . . 6 wff y <RR x
13	12, 9, 1	wral 2475	. . . . 5 wff A. y e. A y <RR x
14	13, 4, 2	wrex 2476	. . . 4 wff E. x e. RR A. y e. A y <RR x
15	5, 10, 11	wbr 4034	. . . . . . 7 wff x <RR y
16		vz	. . . . . . . . . . 11 setvar z
17	16	cv 1363	. . . . . . . . . 10 class z
18	5, 17, 11	wbr 4034	. . . . . . . . 9 wff x <RR z
19	18, 16, 1	wrex 2476	. . . . . . . 8 wff E. z e. A x <RR z
20	17, 10, 11	wbr 4034	. . . . . . . . 9 wff z <RR y
21	20, 16, 1	wral 2475	. . . . . . . 8 wff A. z e. A z <RR y
22	19, 21	wo 709	. . . . . . 7 wff ( E. z e. A x <RR z \/ A. z e. A z <RR y )
23	15, 22	wi 4	. . . . . 6 wff ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) )
24	23, 9, 2	wral 2475	. . . . 5 wff A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) )
25	24, 4, 2	wral 2475	. . . 4 wff 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 ) )
26	14, 25	wa 104	. . 3 wff ( 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 ) ) )
27	8, 26	wa 104	. 2 wff ( ( 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 ) ) ) )
28	15	wn 3	. . . . 5 wff -. x <RR y
29	28, 9, 1	wral 2475	. . . 4 wff A. y e. A -. x <RR y
30	10, 17, 11	wbr 4034	. . . . . . 7 wff y <RR z
31	30, 16, 1	wrex 2476	. . . . . 6 wff E. z e. A y <RR z
32	12, 31	wi 4	. . . . 5 wff ( y <RR x -> E. z e. A y <RR z )
33	32, 9, 2	wral 2475	. . . 4 wff A. y e. RR ( y <RR x -> E. z e. A y <RR z )
34	29, 33	wa 104	. . 3 wff ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) )
35	34, 4, 2	wrex 2476	. 2 wff 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 ) )
36	27, 35	wi 4	1 wff ( ( ( 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 axiom is referenced by:  axsuploc  8116