Metamath Proof Explorer

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 
|- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E! j e. S A. k e. S j <_ k )

Proof

Step Hyp Ref Expression
1 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
2 zssre 
 |-  ZZ C_ RR
3 1 2 sstri 
 |-  ( ZZ>= ` M ) C_ RR
4 sstr 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ ( ZZ>= ` M ) C_ RR ) -> S C_ RR )
5 3 4 mpan2 
 |-  ( S C_ ( ZZ>= ` M ) -> S C_ RR )
6 uzwo 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. k e. S j <_ k )
7 lbreu 
 |-  ( ( S C_ RR /\ E. j e. S A. k e. S j <_ k ) -> E! j e. S A. k e. S j <_ k )
8 5 6 7 syl2an2r 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E! j e. S A. k e. S j <_ k )