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 ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )

Proof

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