Theorem uzwo2

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

	Ref	Expression
Assertion	uzwo2	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge S\ne \varnothing \right)\to \exists !j\in S\forall k\in Sj\le k$$

Proof

Step	Hyp	Ref	Expression
1		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
2		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
3	1 2	sstri	$$⊢{\mathbb{Z}}_{\ge M}\subseteq ℝ$$
4		sstr	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge {\mathbb{Z}}_{\ge M}\subseteq ℝ\right)\to S\subseteq ℝ$$
5	3 4	mpan2	$$⊢S\subseteq {\mathbb{Z}}_{\ge M}\to S\subseteq ℝ$$
6		uzwo	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge S\ne \varnothing \right)\to \exists j\in S\forall k\in Sj\le k$$
7		lbreu	$$⊢\left(S\subseteq ℝ\wedge \exists j\in S\forall k\in Sj\le k\right)\to \exists !j\in S\forall k\in Sj\le k$$
8	5 6 7	syl2an2r	$$⊢\left(S\subseteq {\mathbb{Z}}_{\ge M}\wedge S\ne \varnothing \right)\to \exists !j\in S\forall k\in Sj\le k$$