Metamath Proof Explorer

Theorem suprzcl

Description: The supremum of a bounded-above set of integers is a member of the set. (Contributed by Paul Chapman, 21-Mar-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion suprzcl ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<∈A

Proof

Step Hyp Ref Expression
1 zssre ⊢ℤ⊆ℝ
2 sstr ⊢A⊆ℤ∧ℤ⊆ℝ→A⊆ℝ
3 1 2 mpan2 ⊢A⊆ℤ→A⊆ℝ
4 suprcl ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<∈ℝ
5 3 4 syl3an1 ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<∈ℝ
6 5 ltm1d ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<−1<supAℝ<
7 peano2rem ⊢supAℝ<∈ℝ→supAℝ<−1∈ℝ
8 4 7 syl ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<−1∈ℝ
9 suprlub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧supAℝ<−1∈ℝ→supAℝ<−1<supAℝ<↔∃z∈AsupAℝ<−1<z
10 8 9 mpdan ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<−1<supAℝ<↔∃z∈AsupAℝ<−1<z
11 3 10 syl3an1 ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<−1<supAℝ<↔∃z∈AsupAℝ<−1<z
12 6 11 mpbid ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→∃z∈AsupAℝ<−1<z
13 simpl1 ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→A⊆ℤ
14 13 sselda ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→w∈ℤ
15 1 14 sselid ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→w∈ℝ
16 5 adantr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<∈ℝ
17 16 adantr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→supAℝ<∈ℝ
18 simprl ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→z∈A
19 13 18 sseldd ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→z∈ℤ
20 zre ⊢z∈ℤ→z∈ℝ
21 19 20 syl ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→z∈ℝ
22 peano2re ⊢z∈ℝ→z+1∈ℝ
23 21 22 syl ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→z+1∈ℝ
24 23 adantr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→z+1∈ℝ
25 suprub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧w∈A→w≤supAℝ<
26 3 25 syl3anl1 ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧w∈A→w≤supAℝ<
27 26 adantlr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→w≤supAℝ<
28 simprr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<−1<z
29 1red ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→1∈ℝ
30 16 29 21 ltsubaddd ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<−1<z↔supAℝ<<z+1
31 28 30 mpbid ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<<z+1
32 31 adantr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→supAℝ<<z+1
33 15 17 24 27 32 lelttrd ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→w<z+1
34 19 adantr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→z∈ℤ
35 zleltp1 ⊢w∈ℤ∧z∈ℤ→w≤z↔w<z+1
36 14 34 35 syl2anc ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→w≤z↔w<z+1
37 33 36 mpbird ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z∧w∈A→w≤z
38 37 ralrimiva ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→∀w∈Aw≤z
39 suprleub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈ℝ→supAℝ<≤z↔∀w∈Aw≤z
40 3 39 syl3anl1 ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈ℝ→supAℝ<≤z↔∀w∈Aw≤z
41 21 40 syldan ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<≤z↔∀w∈Aw≤z
42 38 41 mpbird ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<≤z
43 suprub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A→z≤supAℝ<
44 3 43 syl3anl1 ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A→z≤supAℝ<
45 44 adantrr ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→z≤supAℝ<
46 16 21 letri3d ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<=z↔supAℝ<≤z∧z≤supAℝ<
47 42 45 46 mpbir2and ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<=z
48 47 18 eqeltrd ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧z∈A∧supAℝ<−1<z→supAℝ<∈A
49 12 48 rexlimddv ⊢A⊆ℤ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<∈A