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

Metamath Proof Explorer

Theorem suprzcl2

Description: The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl avoids ax-pre-sup .) (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion suprzcl2 ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → sup A ℝ < ∈ A

Proof

Step Hyp Ref Expression
1 zsupss ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z
2 ssel2 ⊢ A ⊆ ℤ ∧ x ∈ A → x ∈ ℤ
3 2 zred ⊢ A ⊆ ℤ ∧ x ∈ A → x ∈ ℝ
4 ltso ⊢ < Or ℝ
5 4 a1i ⊢ ⊤ → < Or ℝ
6 5 eqsup ⊢ ⊤ → x ∈ ℝ ∧ ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z → sup A ℝ < = x
7 6 mptru ⊢ x ∈ ℝ ∧ ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z → sup A ℝ < = x
8 7 3expib ⊢ x ∈ ℝ → ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z → sup A ℝ < = x
9 3 8 syl ⊢ A ⊆ ℤ ∧ x ∈ A → ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z → sup A ℝ < = x
10 simpr ⊢ A ⊆ ℤ ∧ x ∈ A → x ∈ A
11 eleq1 ⊢ sup A ℝ < = x → sup A ℝ < ∈ A ↔ x ∈ A
12 10 11 syl5ibrcom ⊢ A ⊆ ℤ ∧ x ∈ A → sup A ℝ < = x → sup A ℝ < ∈ A
13 9 12 syld ⊢ A ⊆ ℤ ∧ x ∈ A → ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z → sup A ℝ < ∈ A
14 13 rexlimdva ⊢ A ⊆ ℤ → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z → sup A ℝ < ∈ A
15 14 3ad2ant1 ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ A y < z → sup A ℝ < ∈ A
16 1 15 mpd ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → sup A ℝ < ∈ A