Axiom ax-ddkcomp 14024

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 14024 should be used in place of construction specific results. In particular, axcaucvg 7862 should be proved from it. (Contributed by BJ, 24-Oct-2021.)

Assertion

Ref	Expression
ax-ddkcomp	⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)))

Detailed syntax breakdown of Axiom ax-ddkcomp

Step	Hyp	Ref	Expression
1		cA	. . . . 5 class 𝐴
2		cr 7773	. . . . 5 class ℝ
3	1, 2	wss 3121	. . . 4 wff 𝐴 ⊆ ℝ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1347	. . . . . 6 class 𝑥
6	5, 1	wcel 2141	. . . . 5 wff 𝑥 ∈ 𝐴
7	6, 4	wex 1485	. . . 4 wff ∃𝑥 𝑥 ∈ 𝐴
8	3, 7	wa 103	. . 3 wff (𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴)
9		vy	. . . . . . 7 setvar 𝑦
10	9	cv 1347	. . . . . 6 class 𝑦
11		clt 7954	. . . . . 6 class <
12	10, 5, 11	wbr 3989	. . . . 5 wff 𝑦 < 𝑥
13	12, 9, 1	wral 2448	. . . 4 wff ∀𝑦 ∈ 𝐴 𝑦 < 𝑥
14	13, 4, 2	wrex 2449	. . 3 wff ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥
15	5, 10, 11	wbr 3989	. . . . . 6 wff 𝑥 < 𝑦
16		vz	. . . . . . . . . 10 setvar 𝑧
17	16	cv 1347	. . . . . . . . 9 class 𝑧
18	5, 17, 11	wbr 3989	. . . . . . . 8 wff 𝑥 < 𝑧
19	18, 16, 1	wrex 2449	. . . . . . 7 wff ∃𝑧 ∈ 𝐴 𝑥 < 𝑧
20	17, 10, 11	wbr 3989	. . . . . . . 8 wff 𝑧 < 𝑦
21	20, 16, 1	wral 2448	. . . . . . 7 wff ∀𝑧 ∈ 𝐴 𝑧 < 𝑦
22	19, 21	wo 703	. . . . . 6 wff (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)
23	15, 22	wi 4	. . . . 5 wff (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))
24	23, 9, 2	wral 2448	. . . 4 wff ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))
25	24, 4, 2	wral 2448	. . 3 wff ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))
26	8, 14, 25	w3a 973	. 2 wff ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦)))
27		cle 7955	. . . . . 6 class ≤
28	10, 5, 27	wbr 3989	. . . . 5 wff 𝑦 ≤ 𝑥
29	28, 9, 1	wral 2448	. . . 4 wff ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥
30		cB	. . . . . . 7 class 𝐵
31		cR	. . . . . . 7 class 𝑅
32	30, 31	wcel 2141	. . . . . 6 wff 𝐵 ∈ 𝑅
33	10, 30, 27	wbr 3989	. . . . . . 7 wff 𝑦 ≤ 𝐵
34	33, 9, 1	wral 2448	. . . . . 6 wff ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵
35	32, 34	wa 103	. . . . 5 wff (𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵)
36	5, 30, 27	wbr 3989	. . . . 5 wff 𝑥 ≤ 𝐵
37	35, 36	wi 4	. . . 4 wff ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)
38	29, 37	wa 103	. . 3 wff (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))
39	38, 4, 2	wrex 2449	. 2 wff ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))
40	26, 39	wi 4	1 wff (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)))

This axiom is referenced by: (None)