Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-arch GIF version

Axiom ax-arch 7157
 Description: Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 7119. This axiom should not be used directly; instead use arch 8352 (which is the same, but stated in terms of ℕ and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)
Assertion
Ref Expression
ax-arch (𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
Distinct variable group:   𝐴,𝑛,𝑥,𝑦

Detailed syntax breakdown of Axiom ax-arch
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cr 7042 . . 3 class
31, 2wcel 1434 . 2 wff 𝐴 ∈ ℝ
4 vn . . . . 5 setvar 𝑛
54cv 1284 . . . 4 class 𝑛
6 cltrr 7047 . . . 4 class <
71, 5, 6wbr 3793 . . 3 wff 𝐴 < 𝑛
8 c1 7044 . . . . . . 7 class 1
9 vx . . . . . . . 8 setvar 𝑥
109cv 1284 . . . . . . 7 class 𝑥
118, 10wcel 1434 . . . . . 6 wff 1 ∈ 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1284 . . . . . . . . 9 class 𝑦
14 caddc 7046 . . . . . . . . 9 class +
1513, 8, 14co 5543 . . . . . . . 8 class (𝑦 + 1)
1615, 10wcel 1434 . . . . . . 7 wff (𝑦 + 1) ∈ 𝑥
1716, 12, 10wral 2349 . . . . . 6 wff 𝑦𝑥 (𝑦 + 1) ∈ 𝑥
1811, 17wa 102 . . . . 5 wff (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)
1918, 9cab 2068 . . . 4 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
2019cint 3644 . . 3 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
217, 4, 20wrex 2350 . 2 wff 𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛
223, 21wi 4 1 wff (𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
 Colors of variables: wff set class This axiom is referenced by:  arch  8352
 Copyright terms: Public domain W3C validator