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

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 ( 𝐴 , ℝ , < ) )