# Metamath Proof Explorer

## Theorem uzwo

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005)

Ref Expression
Assertion uzwo ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {S}\ne \varnothing \right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {k}$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{h}={M}\to \left({h}\le {t}↔{M}\le {t}\right)$
2 1 ralbidv ${⊢}{h}={M}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{M}\le {t}\right)$
3 2 imbi2d ${⊢}{h}={M}\to \left(\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}\right)↔\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{M}\le {t}\right)\right)$
4 breq1 ${⊢}{h}={m}\to \left({h}\le {t}↔{m}\le {t}\right)$
5 4 ralbidv ${⊢}{h}={m}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\right)$
6 5 imbi2d ${⊢}{h}={m}\to \left(\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}\right)↔\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\right)\right)$
7 breq1 ${⊢}{h}={m}+1\to \left({h}\le {t}↔{m}+1\le {t}\right)$
8 7 ralbidv ${⊢}{h}={m}+1\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)$
9 8 imbi2d ${⊢}{h}={m}+1\to \left(\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}\right)↔\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)\right)$
10 breq1 ${⊢}{h}={n}\to \left({h}\le {t}↔{n}\le {t}\right)$
11 10 ralbidv ${⊢}{h}={n}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\right)$
12 11 imbi2d ${⊢}{h}={n}\to \left(\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{h}\le {t}\right)↔\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\right)\right)$
13 ssel ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \left({t}\in {S}\to {t}\in {ℤ}_{\ge {M}}\right)$
14 eluzle ${⊢}{t}\in {ℤ}_{\ge {M}}\to {M}\le {t}$
15 13 14 syl6 ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \left({t}\in {S}\to {M}\le {t}\right)$
16 15 ralrimiv ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{M}\le {t}$
17 16 adantr ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{M}\le {t}$
18 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
19 sstr ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {ℤ}_{\ge {M}}\subseteq ℤ\right)\to {S}\subseteq ℤ$
20 18 19 mpan2 ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to {S}\subseteq ℤ$
21 eluzelz ${⊢}{m}\in {ℤ}_{\ge {M}}\to {m}\in ℤ$
22 breq1 ${⊢}{j}={m}\to \left({j}\le {t}↔{m}\le {t}\right)$
23 22 ralbidv ${⊢}{j}={m}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\right)$
24 23 rspcev ${⊢}\left({m}\in {S}\wedge \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}$
25 24 expcom ${⊢}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \left({m}\in {S}\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)$
26 25 con3rr3 ${⊢}¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to ¬{m}\in {S}\right)$
27 ssel2 ${⊢}\left({S}\subseteq ℤ\wedge {t}\in {S}\right)\to {t}\in ℤ$
28 zre ${⊢}{m}\in ℤ\to {m}\in ℝ$
29 zre ${⊢}{t}\in ℤ\to {t}\in ℝ$
30 letri3 ${⊢}\left({m}\in ℝ\wedge {t}\in ℝ\right)\to \left({m}={t}↔\left({m}\le {t}\wedge {t}\le {m}\right)\right)$
31 28 29 30 syl2an ${⊢}\left({m}\in ℤ\wedge {t}\in ℤ\right)\to \left({m}={t}↔\left({m}\le {t}\wedge {t}\le {m}\right)\right)$
32 zleltp1 ${⊢}\left({t}\in ℤ\wedge {m}\in ℤ\right)\to \left({t}\le {m}↔{t}<{m}+1\right)$
33 peano2re ${⊢}{m}\in ℝ\to {m}+1\in ℝ$
34 28 33 syl ${⊢}{m}\in ℤ\to {m}+1\in ℝ$
35 ltnle ${⊢}\left({t}\in ℝ\wedge {m}+1\in ℝ\right)\to \left({t}<{m}+1↔¬{m}+1\le {t}\right)$
36 29 34 35 syl2an ${⊢}\left({t}\in ℤ\wedge {m}\in ℤ\right)\to \left({t}<{m}+1↔¬{m}+1\le {t}\right)$
37 32 36 bitrd ${⊢}\left({t}\in ℤ\wedge {m}\in ℤ\right)\to \left({t}\le {m}↔¬{m}+1\le {t}\right)$
38 37 ancoms ${⊢}\left({m}\in ℤ\wedge {t}\in ℤ\right)\to \left({t}\le {m}↔¬{m}+1\le {t}\right)$
39 38 anbi2d ${⊢}\left({m}\in ℤ\wedge {t}\in ℤ\right)\to \left(\left({m}\le {t}\wedge {t}\le {m}\right)↔\left({m}\le {t}\wedge ¬{m}+1\le {t}\right)\right)$
40 31 39 bitrd ${⊢}\left({m}\in ℤ\wedge {t}\in ℤ\right)\to \left({m}={t}↔\left({m}\le {t}\wedge ¬{m}+1\le {t}\right)\right)$
41 27 40 sylan2 ${⊢}\left({m}\in ℤ\wedge \left({S}\subseteq ℤ\wedge {t}\in {S}\right)\right)\to \left({m}={t}↔\left({m}\le {t}\wedge ¬{m}+1\le {t}\right)\right)$
42 eleq1a ${⊢}{t}\in {S}\to \left({m}={t}\to {m}\in {S}\right)$
43 42 ad2antll ${⊢}\left({m}\in ℤ\wedge \left({S}\subseteq ℤ\wedge {t}\in {S}\right)\right)\to \left({m}={t}\to {m}\in {S}\right)$
44 41 43 sylbird ${⊢}\left({m}\in ℤ\wedge \left({S}\subseteq ℤ\wedge {t}\in {S}\right)\right)\to \left(\left({m}\le {t}\wedge ¬{m}+1\le {t}\right)\to {m}\in {S}\right)$
45 44 expd ${⊢}\left({m}\in ℤ\wedge \left({S}\subseteq ℤ\wedge {t}\in {S}\right)\right)\to \left({m}\le {t}\to \left(¬{m}+1\le {t}\to {m}\in {S}\right)\right)$
46 con1 ${⊢}\left(¬{m}+1\le {t}\to {m}\in {S}\right)\to \left(¬{m}\in {S}\to {m}+1\le {t}\right)$
47 45 46 syl6 ${⊢}\left({m}\in ℤ\wedge \left({S}\subseteq ℤ\wedge {t}\in {S}\right)\right)\to \left({m}\le {t}\to \left(¬{m}\in {S}\to {m}+1\le {t}\right)\right)$
48 47 com23 ${⊢}\left({m}\in ℤ\wedge \left({S}\subseteq ℤ\wedge {t}\in {S}\right)\right)\to \left(¬{m}\in {S}\to \left({m}\le {t}\to {m}+1\le {t}\right)\right)$
49 48 exp32 ${⊢}{m}\in ℤ\to \left({S}\subseteq ℤ\to \left({t}\in {S}\to \left(¬{m}\in {S}\to \left({m}\le {t}\to {m}+1\le {t}\right)\right)\right)\right)$
50 49 com34 ${⊢}{m}\in ℤ\to \left({S}\subseteq ℤ\to \left(¬{m}\in {S}\to \left({t}\in {S}\to \left({m}\le {t}\to {m}+1\le {t}\right)\right)\right)\right)$
51 50 imp41 ${⊢}\left(\left(\left({m}\in ℤ\wedge {S}\subseteq ℤ\right)\wedge ¬{m}\in {S}\right)\wedge {t}\in {S}\right)\to \left({m}\le {t}\to {m}+1\le {t}\right)$
52 51 ralimdva ${⊢}\left(\left({m}\in ℤ\wedge {S}\subseteq ℤ\right)\wedge ¬{m}\in {S}\right)\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)$
53 52 ex ${⊢}\left({m}\in ℤ\wedge {S}\subseteq ℤ\right)\to \left(¬{m}\in {S}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)\right)$
54 26 53 sylan9r ${⊢}\left(\left({m}\in ℤ\wedge {S}\subseteq ℤ\right)\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)\right)$
55 54 pm2.43d ${⊢}\left(\left({m}\in ℤ\wedge {S}\subseteq ℤ\right)\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)$
56 55 expl ${⊢}{m}\in ℤ\to \left(\left({S}\subseteq ℤ\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)\right)$
57 21 56 syl ${⊢}{m}\in {ℤ}_{\ge {M}}\to \left(\left({S}\subseteq ℤ\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)\right)$
58 20 57 sylani ${⊢}{m}\in {ℤ}_{\ge {M}}\to \left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)\right)$
59 58 a2d ${⊢}{m}\in {ℤ}_{\ge {M}}\to \left(\left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}\le {t}\right)\to \left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{m}+1\le {t}\right)\right)$
60 3 6 9 12 17 59 uzind4i ${⊢}{n}\in {ℤ}_{\ge {M}}\to \left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\right)$
61 breq1 ${⊢}{j}={n}\to \left({j}\le {t}↔{n}\le {t}\right)$
62 61 ralbidv ${⊢}{j}={n}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\right)$
63 62 rspcev ${⊢}\left({n}\in {S}\wedge \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}$
64 63 expcom ${⊢}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\to \left({n}\in {S}\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)$
65 64 con3rr3 ${⊢}¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\to ¬{n}\in {S}\right)$
66 65 adantl ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to \left(\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{n}\le {t}\to ¬{n}\in {S}\right)$
67 60 66 sylcom ${⊢}{n}\in {ℤ}_{\ge {M}}\to \left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to ¬{n}\in {S}\right)$
68 ssel ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \left({n}\in {S}\to {n}\in {ℤ}_{\ge {M}}\right)$
69 68 con3rr3 ${⊢}¬{n}\in {ℤ}_{\ge {M}}\to \left({S}\subseteq {ℤ}_{\ge {M}}\to ¬{n}\in {S}\right)$
70 69 adantrd ${⊢}¬{n}\in {ℤ}_{\ge {M}}\to \left(\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to ¬{n}\in {S}\right)$
71 67 70 pm2.61i ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge ¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)\to ¬{n}\in {S}$
72 71 ex ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \left(¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\to ¬{n}\in {S}\right)$
73 72 alrimdv ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \left(¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\to \forall {n}\phantom{\rule{.4em}{0ex}}¬{n}\in {S}\right)$
74 eq0 ${⊢}{S}=\varnothing ↔\forall {n}\phantom{\rule{.4em}{0ex}}¬{n}\in {S}$
75 73 74 syl6ibr ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \left(¬\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\to {S}=\varnothing \right)$
76 75 necon1ad ${⊢}{S}\subseteq {ℤ}_{\ge {M}}\to \left({S}\ne \varnothing \to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}\right)$
77 76 imp ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {S}\ne \varnothing \right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}$
78 breq2 ${⊢}{t}={k}\to \left({j}\le {t}↔{j}\le {k}\right)$
79 78 cbvralvw ${⊢}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}↔\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {k}$
80 79 rexbii ${⊢}\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {t}↔\exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {k}$
81 77 80 sylib ${⊢}\left({S}\subseteq {ℤ}_{\ge {M}}\wedge {S}\ne \varnothing \right)\to \exists {j}\in {S}\phantom{\rule{.4em}{0ex}}\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}{j}\le {k}$