Metamath Proof Explorer

Theorem sup3

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

Ref Expression
Assertion sup3 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → ∃ x ∈ ℝ ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z

Proof

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