Metamath Proof Explorer


Theorem suprzub

Description: The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Assertion suprzub ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → 𝐴 ⊆ ℤ )
2 zssre ℤ ⊆ ℝ
3 1 2 sstrdi ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → 𝐴 ⊆ ℝ )
4 simp3 ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → 𝐵𝐴 )
5 3 4 sseldd ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → 𝐵 ∈ ℝ )
6 4 ne0d ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → 𝐴 ≠ ∅ )
7 simp2 ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥 )
8 suprzcl2 ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
9 1 6 7 8 syl3anc ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
10 3 9 sseldd ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
11 ltso < Or ℝ
12 11 a1i ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → < Or ℝ )
13 zsupss ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥 ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
14 1 6 7 13 syl3anc ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
15 ssrexv ( 𝐴 ⊆ ℝ → ( ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
16 3 14 15 sylc ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
17 12 16 supub ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → ( 𝐵𝐴 → ¬ sup ( 𝐴 , ℝ , < ) < 𝐵 ) )
18 4 17 mpd ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → ¬ sup ( 𝐴 , ℝ , < ) < 𝐵 )
19 5 10 18 nltled ( ( 𝐴 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦𝐴 𝑦𝑥𝐵𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )