Metamath Proof Explorer


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 )