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