Metamath Proof Explorer

Axiom ax-pre-sup

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 . Note: Normally new proofs would use axsup . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-sup ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y < ℝ x → ∃ x ∈ ℝ ∀ y ∈ A ¬ x < ℝ y ∧ ∀ y ∈ ℝ y < ℝ x → ∃ z ∈ A y < ℝ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cr class ℝ
2 0 1 wss wff A ⊆ ℝ
3 c0 class ∅
4 0 3 wne wff A ≠ ∅
5 vx setvar x
6 vy setvar y
7 6 cv setvar y
8 cltrr class < ℝ
9 5 cv setvar x
10 7 9 8 wbr wff y < ℝ x
11 10 6 0 wral wff ∀ y ∈ A y < ℝ x
12 11 5 1 wrex wff ∃ x ∈ ℝ ∀ y ∈ A y < ℝ x
13 2 4 12 w3a wff A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y < ℝ x
14 9 7 8 wbr wff x < ℝ y
15 14 wn wff ¬ x < ℝ y
16 15 6 0 wral wff ∀ y ∈ A ¬ x < ℝ y
17 vz setvar z
18 17 cv setvar z
19 7 18 8 wbr wff y < ℝ z
20 19 17 0 wrex wff ∃ z ∈ A y < ℝ z
21 10 20 wi wff y < ℝ x → ∃ z ∈ A y < ℝ z
22 21 6 1 wral wff ∀ y ∈ ℝ y < ℝ x → ∃ z ∈ A y < ℝ z
23 16 22 wa wff ∀ y ∈ A ¬ x < ℝ y ∧ ∀ y ∈ ℝ y < ℝ x → ∃ z ∈ A y < ℝ z
24 23 5 1 wrex wff ∃ x ∈ ℝ ∀ y ∈ A ¬ x < ℝ y ∧ ∀ y ∈ ℝ y < ℝ x → ∃ z ∈ A y < ℝ z
25 13 24 wi wff A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y < ℝ x → ∃ x ∈ ℝ ∀ y ∈ A ¬ x < ℝ y ∧ ∀ y ∈ ℝ y < ℝ x → ∃ z ∈ A y < ℝ z