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 ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→B≤supAℝ<

Proof

Step Hyp Ref Expression
1 simp1 ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→A⊆ℤ
2 zssre ⊢ℤ⊆ℝ
3 1 2 sstrdi ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→A⊆ℝ
4 simp3 ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→B∈A
5 3 4 sseldd ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→B∈ℝ
6 4 ne0d ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→A≠∅
7 simp2 ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→∃x∈ℤ∀y∈Ay≤x
8 suprzcl2 ⊢A⊆ℤ∧A≠∅∧∃x∈ℤ∀y∈Ay≤x→supAℝ<∈A
9 1 6 7 8 syl3anc ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→supAℝ<∈A
10 3 9 sseldd ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→supAℝ<∈ℝ
11 ltso ⊢<Orℝ
12 11 a1i ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→<Orℝ
13 zsupss ⊢A⊆ℤ∧A≠∅∧∃x∈ℤ∀y∈Ay≤x→∃x∈A∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z
14 1 6 7 13 syl3anc ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→∃x∈A∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z
15 ssrexv ⊢A⊆ℝ→∃x∈A∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z→∃x∈ℝ∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z
16 3 14 15 sylc ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→∃x∈ℝ∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z
17 12 16 supub ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→B∈A→¬supAℝ<<B
18 4 17 mpd ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→¬supAℝ<<B
19 5 10 18 nltled ⊢A⊆ℤ∧∃x∈ℤ∀y∈Ay≤x∧B∈A→B≤supAℝ<