MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-pre-sup Structured version   Visualization version   GIF version

Axiom ax-pre-sup 9893
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 9869. Note: Normally new proofs would use axsup 9992. (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
StepHypRef Expression
1 cA . . . 4 class 𝐴
2 cr 9814 . . . 4 class
31, 2wss 3540 . . 3 wff 𝐴 ⊆ ℝ
4 c0 3874 . . . 4 class
51, 4wne 2780 . . 3 wff 𝐴 ≠ ∅
6 vy . . . . . . 7 setvar 𝑦
76cv 1474 . . . . . 6 class 𝑦
8 vx . . . . . . 7 setvar 𝑥
98cv 1474 . . . . . 6 class 𝑥
10 cltrr 9819 . . . . . 6 class <
117, 9, 10wbr 4583 . . . . 5 wff 𝑦 < 𝑥
1211, 6, 1wral 2896 . . . 4 wff 𝑦𝐴 𝑦 < 𝑥
1312, 8, 2wrex 2897 . . 3 wff 𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥
143, 5, 13w3a 1031 . 2 wff (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥)
159, 7, 10wbr 4583 . . . . . 6 wff 𝑥 < 𝑦
1615wn 3 . . . . 5 wff ¬ 𝑥 < 𝑦
1716, 6, 1wral 2896 . . . 4 wff 𝑦𝐴 ¬ 𝑥 < 𝑦
18 vz . . . . . . . . 9 setvar 𝑧
1918cv 1474 . . . . . . . 8 class 𝑧
207, 19, 10wbr 4583 . . . . . . 7 wff 𝑦 < 𝑧
2120, 18, 1wrex 2897 . . . . . 6 wff 𝑧𝐴 𝑦 < 𝑧
2211, 21wi 4 . . . . 5 wff (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)
2322, 6, 2wral 2896 . . . 4 wff 𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)
2417, 23wa 383 . . 3 wff (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))
2524, 8, 2wrex 2897 . 2 wff 𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧))
2614, 25wi 4 1 wff ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
Colors of variables: wff setvar class
This axiom is referenced by:  axsup  9992
  Copyright terms: Public domain W3C validator