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

Axiom ax-arch 7001
Description: Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 6963.

This axiom should not be used directly; instead use arch 8176 (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 6886 . . 3 class
31, 2wcel 1393 . 2 wff 𝐴 ∈ ℝ
4 vn . . . . 5 setvar 𝑛
54cv 1242 . . . 4 class 𝑛
6 cltrr 6891 . . . 4 class <
71, 5, 6wbr 3764 . . 3 wff 𝐴 < 𝑛
8 c1 6888 . . . . . . 7 class 1
9 vx . . . . . . . 8 setvar 𝑥
109cv 1242 . . . . . . 7 class 𝑥
118, 10wcel 1393 . . . . . 6 wff 1 ∈ 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1242 . . . . . . . . 9 class 𝑦
14 caddc 6890 . . . . . . . . 9 class +
1513, 8, 14co 5512 . . . . . . . 8 class (𝑦 + 1)
1615, 10wcel 1393 . . . . . . 7 wff (𝑦 + 1) ∈ 𝑥
1716, 12, 10wral 2306 . . . . . 6 wff 𝑦𝑥 (𝑦 + 1) ∈ 𝑥
1811, 17wa 97 . . . . 5 wff (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)
1918, 9cab 2026 . . . 4 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
2019cint 3615 . . 3 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
217, 4, 20wrex 2307 . 2 wff 𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛
223, 21wi 4 1 wff (𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
Colors of variables: wff set class
This axiom is referenced by:  arch  8176
  Copyright terms: Public domain W3C validator