This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) )

Detailed syntax breakdown

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