Axiom ax-ddkcomp 14601

Description: Axiom of Dedekind completeness for Dedekind real numbers: every inhabited 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 Axiom ax-ddkcomp 14601 should be used in place of construction specific results. In particular, axcaucvg 7896 should be proved from it. (Contributed by BJ, 24-Oct-2021.)

Assertion

Ref	Expression
ax-ddkcomp	|- ( ( ( A C_ RR /\ E. x x e. 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 7807	. . . . 5 class RR
3	1, 2	wss 3129	. . . 4 wff A C_ RR
4		vx	. . . . . . 7 setvar x
5	4	cv 1352	. . . . . 6 class x
6	5, 1	wcel 2148	. . . . 5 wff x e. A
7	6, 4	wex 1492	. . . 4 wff E. x x e. A
8	3, 7	wa 104	. . 3 wff ( A C_ RR /\ E. x x e. A )
9		vy	. . . . . . 7 setvar y
10	9	cv 1352	. . . . . 6 class y
11		clt 7988	. . . . . 6 class <
12	10, 5, 11	wbr 4002	. . . . 5 wff y < x
13	12, 9, 1	wral 2455	. . . 4 wff A. y e. A y < x
14	13, 4, 2	wrex 2456	. . 3 wff E. x e. RR A. y e. A y < x
15	5, 10, 11	wbr 4002	. . . . . 6 wff x < y
16		vz	. . . . . . . . . 10 setvar z
17	16	cv 1352	. . . . . . . . 9 class z
18	5, 17, 11	wbr 4002	. . . . . . . 8 wff x < z
19	18, 16, 1	wrex 2456	. . . . . . 7 wff E. z e. A x < z
20	17, 10, 11	wbr 4002	. . . . . . . 8 wff z < y
21	20, 16, 1	wral 2455	. . . . . . 7 wff A. z e. A z < y
22	19, 21	wo 708	. . . . . 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, 9, 2	wral 2455	. . . 4 wff A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) )
25	24, 4, 2	wral 2455	. . 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	8, 14, 25	w3a 978	. 2 wff ( ( A C_ RR /\ E. x x e. 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 7989	. . . . . 6 class <_
28	10, 5, 27	wbr 4002	. . . . 5 wff y <_ x
29	28, 9, 1	wral 2455	. . . 4 wff A. y e. A y <_ x
30		cB	. . . . . . 7 class B
31		cR	. . . . . . 7 class R
32	30, 31	wcel 2148	. . . . . 6 wff B e. R
33	10, 30, 27	wbr 4002	. . . . . . 7 wff y <_ B
34	33, 9, 1	wral 2455	. . . . . 6 wff A. y e. A y <_ B
35	32, 34	wa 104	. . . . 5 wff ( B e. R /\ A. y e. A y <_ B )
36	5, 30, 27	wbr 4002	. . . . 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 104	. . 3 wff ( A. y e. A y <_ x /\ ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B ) )
39	38, 4, 2	wrex 2456	. 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 /\ E. x x e. 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)