Theorem sup3

Description: A version of the completeness axiom for reals. Dual of infm3 . (Contributed by NM, 12-Oct-2004)

	Ref	Expression
Assertion	sup3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
2		leloe	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
3	2	expcom	⊢ ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ℝ → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) )
4	1 3	syl9	⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦 ∈ 𝐴 → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) ) )
5	4	imp31	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
6	5	ralbidva	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
7	6	rexbidva	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
8	7	anbi2d	⊢ ( 𝐴 ⊆ ℝ → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ↔ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) )
9	8	pm5.32i	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) )
10		3anass	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) )
11		3anass	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) )
12	9 10 11	3bitr4i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ↔ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
13		sup2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
14	12 13	sylbi	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )