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

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

This axiom should not be used directly; instead use arch 8606 (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 7296 . . 3 class
31, 2wcel 1436 . 2 wff 𝐴 ∈ ℝ
4 vn . . . . 5 setvar 𝑛
54cv 1286 . . . 4 class 𝑛
6 cltrr 7301 . . . 4 class <
71, 5, 6wbr 3822 . . 3 wff 𝐴 < 𝑛
8 c1 7298 . . . . . . 7 class 1
9 vx . . . . . . . 8 setvar 𝑥
109cv 1286 . . . . . . 7 class 𝑥
118, 10wcel 1436 . . . . . 6 wff 1 ∈ 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1286 . . . . . . . . 9 class 𝑦
14 caddc 7300 . . . . . . . . 9 class +
1513, 8, 14co 5615 . . . . . . . 8 class (𝑦 + 1)
1615, 10wcel 1436 . . . . . . 7 wff (𝑦 + 1) ∈ 𝑥
1716, 12, 10wral 2355 . . . . . 6 wff 𝑦𝑥 (𝑦 + 1) ∈ 𝑥
1811, 17wa 102 . . . . 5 wff (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)
1918, 9cab 2071 . . . 4 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
2019cint 3673 . . 3 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
217, 4, 20wrex 2356 . 2 wff 𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛
223, 21wi 4 1 wff (𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)
Colors of variables: wff set class
This axiom is referenced by:  arch  8606
  Copyright terms: Public domain W3C validator