Theorem nnwof

Description: Well-ordering principle: any nonempty set of positive integers has a least element. This version allows x and y to be present in A as long as they are effectively not free. (Contributed by NM, 17-Aug-2001) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nnwof.1	|- F/_ x A
	nnwof.2	|- F/_ y A
Assertion	nnwof	|- ( ( A C_ NN /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )

Proof

Step	Hyp	Ref	Expression
1		nnwof.1	|- F/_ x A
2		nnwof.2	|- F/_ y A
3		nnwo	|- ( ( A C_ NN /\ A =/= (/) ) -> E. w e. A A. v e. A w <_ v )
4		nfcv	|- F/_ w A
5		nfv	|- F/ x w <_ v
6	1 5	nfralw	|- F/ x A. v e. A w <_ v
7		nfv	|- F/ w A. y e. A x <_ y
8		breq1	|- ( w = x -> ( w <_ v <-> x <_ v ) )
9	8	ralbidv	|- ( w = x -> ( A. v e. A w <_ v <-> A. v e. A x <_ v ) )
10		nfcv	|- F/_ v A
11		nfv	|- F/ y x <_ v
12		nfv	|- F/ v x <_ y
13		breq2	|- ( v = y -> ( x <_ v <-> x <_ y ) )
14	10 2 11 12 13	cbvralfw	|- ( A. v e. A x <_ v <-> A. y e. A x <_ y )
15	9 14	bitrdi	|- ( w = x -> ( A. v e. A w <_ v <-> A. y e. A x <_ y ) )
16	4 1 6 7 15	cbvrexfw	|- ( E. w e. A A. v e. A w <_ v <-> E. x e. A A. y e. A x <_ y )
17	3 16	sylib	|- ( ( A C_ NN /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )