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