Theorem nnwo

Description: Well-ordering principle: any nonempty set of positive integers has a least element. Theorem I.37 (well-ordering principle) of Apostol p. 34. (Contributed by NM, 17-Aug-2001)

	Ref	Expression
Assertion	nnwo	|- ( ( A C_ NN /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )

Proof

Step	Hyp	Ref	Expression
1		nnuz	|- NN = ( ZZ>= ` 1 )
2	1	sseq2i	|- ( A C_ NN <-> A C_ ( ZZ>= ` 1 ) )
3		uzwo	|- ( ( A C_ ( ZZ>= ` 1 ) /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )
4	2 3	sylanb	|- ( ( A C_ NN /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )