# 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 ${⊢}\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{y}={m}\to \left({y}\le {x}↔{m}\le {x}\right)$
2 1 cbvralvw ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}↔\forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {x}$
3 breq2 ${⊢}{x}={n}\to \left({m}\le {x}↔{m}\le {n}\right)$
4 3 ralbidv ${⊢}{x}={n}\to \left(\forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {x}↔\forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)$
5 2 4 syl5bb ${⊢}{x}={n}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}↔\forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)$
6 5 cbvrexvw ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}$
7 simp1rl ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to {n}\in ℤ$
8 7 znegcld ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to -{n}\in ℤ$
9 simp2 ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to {w}\in ℤ$
10 9 zred ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to {w}\in ℝ$
11 7 zred ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to {n}\in ℝ$
12 breq1 ${⊢}{m}=-{w}\to \left({m}\le {n}↔-{w}\le {n}\right)$
13 simp1rr ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}$
14 simp3 ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to -{w}\in {A}$
15 12 13 14 rspcdva ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to -{w}\le {n}$
16 10 11 15 lenegcon1d ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to -{n}\le {w}$
17 eluz2 ${⊢}{w}\in {ℤ}_{\ge \left(-{n}\right)}↔\left(-{n}\in ℤ\wedge {w}\in ℤ\wedge -{n}\le {w}\right)$
18 8 9 16 17 syl3anbrc ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {w}\in ℤ\wedge -{w}\in {A}\right)\to {w}\in {ℤ}_{\ge \left(-{n}\right)}$
19 18 rabssdv ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to \left\{{w}\in ℤ|-{w}\in {A}\right\}\subseteq {ℤ}_{\ge \left(-{n}\right)}$
20 n0 ${⊢}{A}\ne \varnothing ↔\exists {n}\phantom{\rule{.4em}{0ex}}{n}\in {A}$
21 ssel2 ${⊢}\left({A}\subseteq ℤ\wedge {n}\in {A}\right)\to {n}\in ℤ$
22 21 znegcld ${⊢}\left({A}\subseteq ℤ\wedge {n}\in {A}\right)\to -{n}\in ℤ$
23 21 zcnd ${⊢}\left({A}\subseteq ℤ\wedge {n}\in {A}\right)\to {n}\in ℂ$
24 23 negnegd ${⊢}\left({A}\subseteq ℤ\wedge {n}\in {A}\right)\to -\left(-{n}\right)={n}$
25 simpr ${⊢}\left({A}\subseteq ℤ\wedge {n}\in {A}\right)\to {n}\in {A}$
26 24 25 eqeltrd ${⊢}\left({A}\subseteq ℤ\wedge {n}\in {A}\right)\to -\left(-{n}\right)\in {A}$
27 negeq ${⊢}{w}=-{n}\to -{w}=-\left(-{n}\right)$
28 27 eleq1d ${⊢}{w}=-{n}\to \left(-{w}\in {A}↔-\left(-{n}\right)\in {A}\right)$
29 28 rspcev ${⊢}\left(-{n}\in ℤ\wedge -\left(-{n}\right)\in {A}\right)\to \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}$
30 22 26 29 syl2anc ${⊢}\left({A}\subseteq ℤ\wedge {n}\in {A}\right)\to \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}$
31 30 ex ${⊢}{A}\subseteq ℤ\to \left({n}\in {A}\to \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}\right)$
32 31 exlimdv ${⊢}{A}\subseteq ℤ\to \left(\exists {n}\phantom{\rule{.4em}{0ex}}{n}\in {A}\to \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}\right)$
33 32 imp ${⊢}\left({A}\subseteq ℤ\wedge \exists {n}\phantom{\rule{.4em}{0ex}}{n}\in {A}\right)\to \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}$
34 20 33 sylan2b ${⊢}\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\to \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}$
35 34 adantr ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}$
36 rabn0 ${⊢}\left\{{w}\in ℤ|-{w}\in {A}\right\}\ne \varnothing ↔\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}-{w}\in {A}$
37 35 36 sylibr ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to \left\{{w}\in ℤ|-{w}\in {A}\right\}\ne \varnothing$
38 infssuzcl ${⊢}\left(\left\{{w}\in ℤ|-{w}\in {A}\right\}\subseteq {ℤ}_{\ge \left(-{n}\right)}\wedge \left\{{w}\in ℤ|-{w}\in {A}\right\}\ne \varnothing \right)\to sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in \left\{{w}\in ℤ|-{w}\in {A}\right\}$
39 19 37 38 syl2anc ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in \left\{{w}\in ℤ|-{w}\in {A}\right\}$
40 negeq ${⊢}{n}=sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to -{n}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)$
41 40 eleq1d ${⊢}{n}=sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left(-{n}\in {A}↔-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in {A}\right)$
42 negeq ${⊢}{w}={n}\to -{w}=-{n}$
43 42 eleq1d ${⊢}{w}={n}\to \left(-{w}\in {A}↔-{n}\in {A}\right)$
44 43 cbvrabv ${⊢}\left\{{w}\in ℤ|-{w}\in {A}\right\}=\left\{{n}\in ℤ|-{n}\in {A}\right\}$
45 41 44 elrab2 ${⊢}sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in \left\{{w}\in ℤ|-{w}\in {A}\right\}↔\left(sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in ℤ\wedge -sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in {A}\right)$
46 45 simprbi ${⊢}sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in \left\{{w}\in ℤ|-{w}\in {A}\right\}\to -sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in {A}$
47 39 46 syl ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to -sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in {A}$
48 simpll ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to {A}\subseteq ℤ$
49 48 sselda ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to {y}\in ℤ$
50 49 zred ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to {y}\in ℝ$
51 ssrab2 ${⊢}\left\{{w}\in ℤ|-{w}\in {A}\right\}\subseteq ℤ$
52 39 adantr ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in \left\{{w}\in ℤ|-{w}\in {A}\right\}$
53 51 52 sseldi ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in ℤ$
54 53 znegcld ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to -sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in ℤ$
55 54 zred ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to -sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in ℝ$
56 53 zred ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in ℝ$
57 19 adantr ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to \left\{{w}\in ℤ|-{w}\in {A}\right\}\subseteq {ℤ}_{\ge \left(-{n}\right)}$
58 negeq ${⊢}{w}=-{y}\to -{w}=-\left(-{y}\right)$
59 58 eleq1d ${⊢}{w}=-{y}\to \left(-{w}\in {A}↔-\left(-{y}\right)\in {A}\right)$
60 49 znegcld ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to -{y}\in ℤ$
61 49 zcnd ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to {y}\in ℂ$
62 61 negnegd ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to -\left(-{y}\right)={y}$
63 simpr ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to {y}\in {A}$
64 62 63 eqeltrd ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to -\left(-{y}\right)\in {A}$
65 59 60 64 elrabd ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to -{y}\in \left\{{w}\in ℤ|-{w}\in {A}\right\}$
66 infssuzle ${⊢}\left(\left\{{w}\in ℤ|-{w}\in {A}\right\}\subseteq {ℤ}_{\ge \left(-{n}\right)}\wedge -{y}\in \left\{{w}\in ℤ|-{w}\in {A}\right\}\right)\to sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\le -{y}$
67 57 65 66 syl2anc ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\le -{y}$
68 56 50 67 lenegcon2d ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to {y}\le -sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)$
69 50 55 68 lensymd ${⊢}\left(\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\wedge {y}\in {A}\right)\to ¬-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)<{y}$
70 69 ralrimiva ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)<{y}$
71 breq2 ${⊢}{z}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left({y}<{z}↔{y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\right)$
72 71 rspcev ${⊢}\left(-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in {A}\wedge {y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}$
73 72 ex ${⊢}-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in {A}\to \left({y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
74 47 73 syl ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to \left({y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
75 74 ralrimivw ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
76 breq1 ${⊢}{x}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left({x}<{y}↔-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)<{y}\right)$
77 76 notbid ${⊢}{x}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left(¬{x}<{y}↔¬-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)<{y}\right)$
78 77 ralbidv ${⊢}{x}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)<{y}\right)$
79 breq2 ${⊢}{x}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left({y}<{x}↔{y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\right)$
80 79 imbi1d ${⊢}{x}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left(\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\left({y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
81 80 ralbidv ${⊢}{x}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
82 78 81 anbi12d ${⊢}{x}=-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
83 82 rspcev ${⊢}\left(-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\in {A}\wedge \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<-sup\left(\left\{{w}\in ℤ|-{w}\in {A}\right\},ℝ,<\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
84 47 70 75 83 syl12anc ${⊢}\left(\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\wedge \left({n}\in ℤ\wedge \forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
85 84 rexlimdvaa ${⊢}\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\to \left(\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {m}\in {A}\phantom{\rule{.4em}{0ex}}{m}\le {n}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
86 6 85 syl5bi ${⊢}\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \right)\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
87 86 3impia ${⊢}\left({A}\subseteq ℤ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$