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

Proof

Step Hyp Ref Expression
1 zsupss ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥 ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
2 ssel2 ( ( 𝐴 ⊆ ℤ ∧ 𝑥𝐴 ) → 𝑥 ∈ ℤ )
3 2 zred ( ( 𝐴 ⊆ ℤ ∧ 𝑥𝐴 ) → 𝑥 ∈ ℝ )
4 ltso < Or ℝ
5 4 a1i ( ⊤ → < Or ℝ )
6 5 eqsup ( ⊤ → ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 ) )
7 6 mptru ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 )
8 7 3expib ( 𝑥 ∈ ℝ → ( ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 ) )
9 3 8 syl ( ( 𝐴 ⊆ ℤ ∧ 𝑥𝐴 ) → ( ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 ) )
10 simpr ( ( 𝐴 ⊆ ℤ ∧ 𝑥𝐴 ) → 𝑥𝐴 )
11 eleq1 ( sup ( 𝐴 , ℝ , < ) = 𝑥 → ( sup ( 𝐴 , ℝ , < ) ∈ 𝐴𝑥𝐴 ) )
12 10 11 syl5ibrcom ( ( 𝐴 ⊆ ℤ ∧ 𝑥𝐴 ) → ( sup ( 𝐴 , ℝ , < ) = 𝑥 → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
13 9 12 syld ( ( 𝐴 ⊆ ℤ ∧ 𝑥𝐴 ) → ( ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
14 13 rexlimdva ( 𝐴 ⊆ ℤ → ( ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
15 14 3ad2ant1 ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥 ) → ( ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
16 1 15 mpd ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )