This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )