Axiom ax-pre-sup 10880

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup 10856. Note: Normally new proofs would use axsup 10981. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)

Assertion

Ref	Expression
ax-pre-sup	⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))

Distinct variable group:   𝑥,𝑦,𝑧,𝐴

Detailed syntax breakdown of Axiom ax-pre-sup

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		cr 10801	. . . 4 class ℝ
3	1, 2	wss 3883	. . 3 wff 𝐴 ⊆ ℝ
4		c0 4253	. . . 4 class ∅
5	1, 4	wne 2942	. . 3 wff 𝐴 ≠ ∅
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1538	. . . . . 6 class 𝑦
8		vx	. . . . . . 7 setvar 𝑥
9	8	cv 1538	. . . . . 6 class 𝑥
10		cltrr 10806	. . . . . 6 class <ℝ
11	7, 9, 10	wbr 5070	. . . . 5 wff 𝑦 <ℝ 𝑥
12	11, 6, 1	wral 3063	. . . 4 wff ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥
13	12, 8, 2	wrex 3064	. . 3 wff ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥
14	3, 5, 13	w3a 1085	. 2 wff (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)
15	9, 7, 10	wbr 5070	. . . . . 6 wff 𝑥 <ℝ 𝑦
16	15	wn 3	. . . . 5 wff ¬ 𝑥 <ℝ 𝑦
17	16, 6, 1	wral 3063	. . . 4 wff ∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦
18		vz	. . . . . . . . 9 setvar 𝑧
19	18	cv 1538	. . . . . . . 8 class 𝑧
20	7, 19, 10	wbr 5070	. . . . . . 7 wff 𝑦 <ℝ 𝑧
21	20, 18, 1	wrex 3064	. . . . . 6 wff ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧
22	11, 21	wi 4	. . . . 5 wff (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)
23	22, 6, 2	wral 3063	. . . 4 wff ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)
24	17, 23	wa 395	. . 3 wff (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))
25	24, 8, 2	wrex 3064	. 2 wff ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))
26	14, 25	wi 4	1 wff ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))

This axiom is referenced by:  axsup  10981