Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  ax-ddkcomp GIF version

Axiom ax-ddkcomp 13240
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 the axiom ax-ddkcomp 13240 should be used in place of construction specific results. In particular, axcaucvg 7715 should be proved from it. (Contributed by BJ, 24-Oct-2021.)
Assertion
Ref Expression
ax-ddkcomp (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵)))

Detailed syntax breakdown of Axiom ax-ddkcomp
StepHypRef Expression
1 cA . . . . 5 class 𝐴
2 cr 7626 . . . . 5 class
31, 2wss 3071 . . . 4 wff 𝐴 ⊆ ℝ
4 vx . . . . . . 7 setvar 𝑥
54cv 1330 . . . . . 6 class 𝑥
65, 1wcel 1480 . . . . 5 wff 𝑥𝐴
76, 4wex 1468 . . . 4 wff 𝑥 𝑥𝐴
83, 7wa 103 . . 3 wff (𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴)
9 vy . . . . . . 7 setvar 𝑦
109cv 1330 . . . . . 6 class 𝑦
11 clt 7807 . . . . . 6 class <
1210, 5, 11wbr 3929 . . . . 5 wff 𝑦 < 𝑥
1312, 9, 1wral 2416 . . . 4 wff 𝑦𝐴 𝑦 < 𝑥
1413, 4, 2wrex 2417 . . 3 wff 𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥
155, 10, 11wbr 3929 . . . . . 6 wff 𝑥 < 𝑦
16 vz . . . . . . . . . 10 setvar 𝑧
1716cv 1330 . . . . . . . . 9 class 𝑧
185, 17, 11wbr 3929 . . . . . . . 8 wff 𝑥 < 𝑧
1918, 16, 1wrex 2417 . . . . . . 7 wff 𝑧𝐴 𝑥 < 𝑧
2017, 10, 11wbr 3929 . . . . . . . 8 wff 𝑧 < 𝑦
2120, 16, 1wral 2416 . . . . . . 7 wff 𝑧𝐴 𝑧 < 𝑦
2219, 21wo 697 . . . . . 6 wff (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦)
2315, 22wi 4 . . . . 5 wff (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))
2423, 9, 2wral 2416 . . . 4 wff 𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))
2524, 4, 2wral 2416 . . 3 wff 𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))
268, 14, 25w3a 962 . 2 wff ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦)))
27 cle 7808 . . . . . 6 class
2810, 5, 27wbr 3929 . . . . 5 wff 𝑦𝑥
2928, 9, 1wral 2416 . . . 4 wff 𝑦𝐴 𝑦𝑥
30 cB . . . . . . 7 class 𝐵
31 cR . . . . . . 7 class 𝑅
3230, 31wcel 1480 . . . . . 6 wff 𝐵𝑅
3310, 30, 27wbr 3929 . . . . . . 7 wff 𝑦𝐵
3433, 9, 1wral 2416 . . . . . 6 wff 𝑦𝐴 𝑦𝐵
3532, 34wa 103 . . . . 5 wff (𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵)
365, 30, 27wbr 3929 . . . . 5 wff 𝑥𝐵
3735, 36wi 4 . . . 4 wff ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵)
3829, 37wa 103 . . 3 wff (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵))
3938, 4, 2wrex 2417 . 2 wff 𝑥 ∈ ℝ (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵))
4026, 39wi 4 1 wff (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵)))
Colors of variables: wff set class
This axiom is referenced by: (None)
  Copyright terms: Public domain W3C validator