Axiom ax-arch 8194

Description: Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 8154.

This axiom should not be used directly; instead use arch 9442 (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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cr 8074	. . 3 class ℝ
3	1, 2	wcel 2202	. 2 wff 𝐴 ∈ ℝ
4		vn	. . . . 5 setvar 𝑛
5	4	cv 1397	. . . 4 class 𝑛
6		cltrr 8079	. . . 4 class <ℝ
7	1, 5, 6	wbr 4093	. . 3 wff 𝐴 <ℝ 𝑛
8		c1 8076	. . . . . . 7 class 1
9		vx	. . . . . . . 8 setvar 𝑥
10	9	cv 1397	. . . . . . 7 class 𝑥
11	8, 10	wcel 2202	. . . . . 6 wff 1 ∈ 𝑥
12		vy	. . . . . . . . . 10 setvar 𝑦
13	12	cv 1397	. . . . . . . . 9 class 𝑦
14		caddc 8078	. . . . . . . . 9 class +
15	13, 8, 14	co 6028	. . . . . . . 8 class (𝑦 + 1)
16	15, 10	wcel 2202	. . . . . . 7 wff (𝑦 + 1) ∈ 𝑥
17	16, 12, 10	wral 2511	. . . . . 6 wff ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥
18	11, 17	wa 104	. . . . 5 wff (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)
19	18, 9	cab 2217	. . . 4 class {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
20	19	cint 3933	. . 3 class ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
21	7, 4, 20	wrex 2512	. 2 wff ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛
22	3, 21	wi 4	1 wff (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)

This axiom is referenced by:  arch  9442