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	⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃! 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )

Proof

Step	Hyp	Ref	Expression
1		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
2		zssre	⊢ ℤ ⊆ ℝ
3	1 2	sstri	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
4		sstr	⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ ) → 𝑆 ⊆ ℝ )
5	3 4	mpan2	⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → 𝑆 ⊆ ℝ )
6		uzwo	⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )
7		lbreu	⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ) → ∃! 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )
8	5 6 7	syl2an2r	⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃! 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )