Metamath Proof Explorer

Theorem zsupss

Description: Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup .) (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Assertion zsupss ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ B y < x → ∃ z ∈ A y < z

Proof

Step Hyp Ref Expression
1 breq1 ⊢ y = m → y ≤ x ↔ m ≤ x
2 1 cbvralvw ⊢ ∀ y ∈ A y ≤ x ↔ ∀ m ∈ A m ≤ x
3 breq2 ⊢ x = n → m ≤ x ↔ m ≤ n
4 3 ralbidv ⊢ x = n → ∀ m ∈ A m ≤ x ↔ ∀ m ∈ A m ≤ n
5 2 4 bitrid ⊢ x = n → ∀ y ∈ A y ≤ x ↔ ∀ m ∈ A m ≤ n
6 5 cbvrexvw ⊢ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x ↔ ∃ n ∈ ℤ ∀ m ∈ A m ≤ n
7 simp1rl ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → n ∈ ℤ
8 7 znegcld ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → − n ∈ ℤ
9 simp2 ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → w ∈ ℤ
10 9 zred ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → w ∈ ℝ
11 7 zred ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → n ∈ ℝ
12 breq1 ⊢ m = − w → m ≤ n ↔ − w ≤ n
13 simp1rr ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → ∀ m ∈ A m ≤ n
14 simp3 ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → − w ∈ A
15 12 13 14 rspcdva ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → − w ≤ n
16 10 11 15 lenegcon1d ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → − n ≤ w
17 eluz2 ⊢ w ∈ ℤ ≥ − n ↔ − n ∈ ℤ ∧ w ∈ ℤ ∧ − n ≤ w
18 8 9 16 17 syl3anbrc ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ w ∈ ℤ ∧ − w ∈ A → w ∈ ℤ ≥ − n
19 18 rabssdv ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → w ∈ ℤ | − w ∈ A ⊆ ℤ ≥ − n
20 n0 ⊢ A ≠ ∅ ↔ ∃ n n ∈ A
21 ssel2 ⊢ A ⊆ ℤ ∧ n ∈ A → n ∈ ℤ
22 21 znegcld ⊢ A ⊆ ℤ ∧ n ∈ A → − n ∈ ℤ
23 21 zcnd ⊢ A ⊆ ℤ ∧ n ∈ A → n ∈ ℂ
24 23 negnegd ⊢ A ⊆ ℤ ∧ n ∈ A → − − n = n
25 simpr ⊢ A ⊆ ℤ ∧ n ∈ A → n ∈ A
26 24 25 eqeltrd ⊢ A ⊆ ℤ ∧ n ∈ A → − − n ∈ A
27 negeq ⊢ w = − n → − w = − − n
28 27 eleq1d ⊢ w = − n → − w ∈ A ↔ − − n ∈ A
29 28 rspcev ⊢ − n ∈ ℤ ∧ − − n ∈ A → ∃ w ∈ ℤ − w ∈ A
30 22 26 29 syl2anc ⊢ A ⊆ ℤ ∧ n ∈ A → ∃ w ∈ ℤ − w ∈ A
31 30 ex ⊢ A ⊆ ℤ → n ∈ A → ∃ w ∈ ℤ − w ∈ A
32 31 exlimdv ⊢ A ⊆ ℤ → ∃ n n ∈ A → ∃ w ∈ ℤ − w ∈ A
33 32 imp ⊢ A ⊆ ℤ ∧ ∃ n n ∈ A → ∃ w ∈ ℤ − w ∈ A
34 20 33 sylan2b ⊢ A ⊆ ℤ ∧ A ≠ ∅ → ∃ w ∈ ℤ − w ∈ A
35 34 adantr ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → ∃ w ∈ ℤ − w ∈ A
36 rabn0 ⊢ w ∈ ℤ | − w ∈ A ≠ ∅ ↔ ∃ w ∈ ℤ − w ∈ A
37 35 36 sylibr ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → w ∈ ℤ | − w ∈ A ≠ ∅
38 infssuzcl ⊢ w ∈ ℤ | − w ∈ A ⊆ ℤ ≥ − n ∧ w ∈ ℤ | − w ∈ A ≠ ∅ → inf w ∈ ℤ | − w ∈ A ℝ < ∈ w ∈ ℤ | − w ∈ A
39 19 37 38 syl2anc ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → inf w ∈ ℤ | − w ∈ A ℝ < ∈ w ∈ ℤ | − w ∈ A
40 negeq ⊢ n = inf w ∈ ℤ | − w ∈ A ℝ < → − n = − inf w ∈ ℤ | − w ∈ A ℝ <
41 40 eleq1d ⊢ n = inf w ∈ ℤ | − w ∈ A ℝ < → − n ∈ A ↔ − inf w ∈ ℤ | − w ∈ A ℝ < ∈ A
42 negeq ⊢ w = n → − w = − n
43 42 eleq1d ⊢ w = n → − w ∈ A ↔ − n ∈ A
44 43 cbvrabv ⊢ w ∈ ℤ | − w ∈ A = n ∈ ℤ | − n ∈ A
45 41 44 elrab2 ⊢ inf w ∈ ℤ | − w ∈ A ℝ < ∈ w ∈ ℤ | − w ∈ A ↔ inf w ∈ ℤ | − w ∈ A ℝ < ∈ ℤ ∧ − inf w ∈ ℤ | − w ∈ A ℝ < ∈ A
46 45 simprbi ⊢ inf w ∈ ℤ | − w ∈ A ℝ < ∈ w ∈ ℤ | − w ∈ A → − inf w ∈ ℤ | − w ∈ A ℝ < ∈ A
47 39 46 syl ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → − inf w ∈ ℤ | − w ∈ A ℝ < ∈ A
48 simpll ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → A ⊆ ℤ
49 48 sselda ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → y ∈ ℤ
50 49 zred ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → y ∈ ℝ
51 ssrab2 ⊢ w ∈ ℤ | − w ∈ A ⊆ ℤ
52 39 adantr ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → inf w ∈ ℤ | − w ∈ A ℝ < ∈ w ∈ ℤ | − w ∈ A
53 51 52 sselid ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → inf w ∈ ℤ | − w ∈ A ℝ < ∈ ℤ
54 53 znegcld ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → − inf w ∈ ℤ | − w ∈ A ℝ < ∈ ℤ
55 54 zred ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → − inf w ∈ ℤ | − w ∈ A ℝ < ∈ ℝ
56 53 zred ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → inf w ∈ ℤ | − w ∈ A ℝ < ∈ ℝ
57 19 adantr ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → w ∈ ℤ | − w ∈ A ⊆ ℤ ≥ − n
58 negeq ⊢ w = − y → − w = − − y
59 58 eleq1d ⊢ w = − y → − w ∈ A ↔ − − y ∈ A
60 49 znegcld ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → − y ∈ ℤ
61 49 zcnd ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → y ∈ ℂ
62 61 negnegd ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → − − y = y
63 simpr ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → y ∈ A
64 62 63 eqeltrd ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → − − y ∈ A
65 59 60 64 elrabd ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → − y ∈ w ∈ ℤ | − w ∈ A
66 infssuzle ⊢ w ∈ ℤ | − w ∈ A ⊆ ℤ ≥ − n ∧ − y ∈ w ∈ ℤ | − w ∈ A → inf w ∈ ℤ | − w ∈ A ℝ < ≤ − y
67 57 65 66 syl2anc ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → inf w ∈ ℤ | − w ∈ A ℝ < ≤ − y
68 56 50 67 lenegcon2d ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → y ≤ − inf w ∈ ℤ | − w ∈ A ℝ <
69 50 55 68 lensymd ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n ∧ y ∈ A → ¬ − inf w ∈ ℤ | − w ∈ A ℝ < < y
70 69 ralrimiva ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → ∀ y ∈ A ¬ − inf w ∈ ℤ | − w ∈ A ℝ < < y
71 breq2 ⊢ z = − inf w ∈ ℤ | − w ∈ A ℝ < → y < z ↔ y < − inf w ∈ ℤ | − w ∈ A ℝ <
72 71 rspcev ⊢ − inf w ∈ ℤ | − w ∈ A ℝ < ∈ A ∧ y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z
73 72 ex ⊢ − inf w ∈ ℤ | − w ∈ A ℝ < ∈ A → y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z
74 47 73 syl ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z
75 74 ralrimivw ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → ∀ y ∈ B y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z
76 breq1 ⊢ x = − inf w ∈ ℤ | − w ∈ A ℝ < → x < y ↔ − inf w ∈ ℤ | − w ∈ A ℝ < < y
77 76 notbid ⊢ x = − inf w ∈ ℤ | − w ∈ A ℝ < → ¬ x < y ↔ ¬ − inf w ∈ ℤ | − w ∈ A ℝ < < y
78 77 ralbidv ⊢ x = − inf w ∈ ℤ | − w ∈ A ℝ < → ∀ y ∈ A ¬ x < y ↔ ∀ y ∈ A ¬ − inf w ∈ ℤ | − w ∈ A ℝ < < y
79 breq2 ⊢ x = − inf w ∈ ℤ | − w ∈ A ℝ < → y < x ↔ y < − inf w ∈ ℤ | − w ∈ A ℝ <
80 79 imbi1d ⊢ x = − inf w ∈ ℤ | − w ∈ A ℝ < → y < x → ∃ z ∈ A y < z ↔ y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z
81 80 ralbidv ⊢ x = − inf w ∈ ℤ | − w ∈ A ℝ < → ∀ y ∈ B y < x → ∃ z ∈ A y < z ↔ ∀ y ∈ B y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z
82 78 81 anbi12d ⊢ x = − inf w ∈ ℤ | − w ∈ A ℝ < → ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ B y < x → ∃ z ∈ A y < z ↔ ∀ y ∈ A ¬ − inf w ∈ ℤ | − w ∈ A ℝ < < y ∧ ∀ y ∈ B y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z
83 82 rspcev ⊢ − inf w ∈ ℤ | − w ∈ A ℝ < ∈ A ∧ ∀ y ∈ A ¬ − inf w ∈ ℤ | − w ∈ A ℝ < < y ∧ ∀ y ∈ B y < − inf w ∈ ℤ | − w ∈ A ℝ < → ∃ z ∈ A y < z → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ B y < x → ∃ z ∈ A y < z
84 47 70 75 83 syl12anc ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ n ∈ ℤ ∧ ∀ m ∈ A m ≤ n → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ B y < x → ∃ z ∈ A y < z
85 84 rexlimdvaa ⊢ A ⊆ ℤ ∧ A ≠ ∅ → ∃ n ∈ ℤ ∀ m ∈ A m ≤ n → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ B y < x → ∃ z ∈ A y < z
86 6 85 biimtrid ⊢ A ⊆ ℤ ∧ A ≠ ∅ → ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ B y < x → ∃ z ∈ A y < z
87 86 3impia ⊢ A ⊆ ℤ ∧ A ≠ ∅ ∧ ∃ x ∈ ℤ ∀ y ∈ A y ≤ x → ∃ x ∈ A ∀ y ∈ A ¬ x < y ∧ ∀ y ∈ B y < x → ∃ z ∈ A y < z