Axiom ax-ddkcomp 10114

Description: Axiom of Dedekind completeness for Dedekind real numbers: every nonempty upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then the axiom ax-ddkcomp 10114 should be used in place of construction specific results. In particular, axcaucvg 6974 should be proved from it. (Contributed by BJ, 24-Oct-2021.)

Assertion

Ref	Expression
ax-ddkcomp	|- ( ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A y < x /\ A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) ) -> E. x e. RR ( A. y e. A y <_ x /\ ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B ) ) )

Detailed syntax breakdown of Axiom ax-ddkcomp

Step	Hyp	Ref	Expression
1		cA	. . . . 5 class A
2		cr 6888	. . . . 5 class RR
3	1, 2	wss 2917	. . . 4 wff A C_ RR
4		c0 3224	. . . . 5 class (/)
5	1, 4	wne 2204	. . . 4 wff A =/= (/)
6	3, 5	wa 97	. . 3 wff ( A C_ RR /\ A =/= (/) )
7		vy	. . . . . . 7 setvar y
8	7	cv 1242	. . . . . 6 class y
9		vx	. . . . . . 7 setvar x
10	9	cv 1242	. . . . . 6 class x
11		clt 7060	. . . . . 6 class <
12	8, 10, 11	wbr 3764	. . . . 5 wff y < x
13	12, 7, 1	wral 2306	. . . 4 wff A. y e. A y < x
14	13, 9, 2	wrex 2307	. . 3 wff E. x e. RR A. y e. A y < x
15	10, 8, 11	wbr 3764	. . . . . 6 wff x < y
16		vz	. . . . . . . . . 10 setvar z
17	16	cv 1242	. . . . . . . . 9 class z
18	10, 17, 11	wbr 3764	. . . . . . . 8 wff x < z
19	18, 16, 1	wrex 2307	. . . . . . 7 wff E. z e. A x < z
20	17, 8, 11	wbr 3764	. . . . . . . 8 wff z < y
21	20, 16, 1	wral 2306	. . . . . . 7 wff A. z e. A z < y
22	19, 21	wo 629	. . . . . 6 wff ( E. z e. A x < z \/ A. z e. A z < y )
23	15, 22	wi 4	. . . . 5 wff ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) )
24	23, 7, 2	wral 2306	. . . 4 wff A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) )
25	24, 9, 2	wral 2306	. . 3 wff A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) )
26	6, 14, 25	w3a 885	. 2 wff ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A y < x /\ A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) )
27		cle 7061	. . . . . 6 class <_
28	8, 10, 27	wbr 3764	. . . . 5 wff y <_ x
29	28, 7, 1	wral 2306	. . . 4 wff A. y e. A y <_ x
30		cB	. . . . . . 7 class B
31		cR	. . . . . . 7 class R
32	30, 31	wcel 1393	. . . . . 6 wff B e. R
33	8, 30, 27	wbr 3764	. . . . . . 7 wff y <_ B
34	33, 7, 1	wral 2306	. . . . . 6 wff A. y e. A y <_ B
35	32, 34	wa 97	. . . . 5 wff ( B e. R /\ A. y e. A y <_ B )
36	10, 30, 27	wbr 3764	. . . . 5 wff x <_ B
37	35, 36	wi 4	. . . 4 wff ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B )
38	29, 37	wa 97	. . 3 wff ( A. y e. A y <_ x /\ ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B ) )
39	38, 9, 2	wrex 2307	. 2 wff E. x e. RR ( A. y e. A y <_ x /\ ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B ) )
40	26, 39	wi 4	1 wff ( ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A y < x /\ A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) ) -> E. x e. RR ( A. y e. A y <_ x /\ ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B ) ) )

This axiom is referenced by: (None)