Metamath Proof Explorer

Theorem nnwos

Description: Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001)

Ref Expression
Hypothesis nnwos.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion nnwos 
|- ( E. x e. NN ph -> E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) )

Proof

Step Hyp Ref Expression
1 nnwos.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 nfrab1 
 |-  F/_ x { x e. NN | ph }
3 nfcv 
 |-  F/_ y { x e. NN | ph }
4 2 3 nnwof 
 |-  ( ( { x e. NN | ph } C_ NN /\ { x e. NN | ph } =/= (/) ) -> E. x e. { x e. NN | ph } A. y e. { x e. NN | ph } x <_ y )
5 ssrab2 
 |-  { x e. NN | ph } C_ NN
6 5 biantrur 
 |-  ( { x e. NN | ph } =/= (/) <-> ( { x e. NN | ph } C_ NN /\ { x e. NN | ph } =/= (/) ) )
7 rabn0 
 |-  ( { x e. NN | ph } =/= (/) <-> E. x e. NN ph )
8 6 7 bitr3i 
 |-  ( ( { x e. NN | ph } C_ NN /\ { x e. NN | ph } =/= (/) ) <-> E. x e. NN ph )
9 df-rex 
 |-  ( E. x e. { x e. NN | ph } A. y e. { x e. NN | ph } x <_ y <-> E. x ( x e. { x e. NN | ph } /\ A. y e. { x e. NN | ph } x <_ y ) )
10 rabid 
 |-  ( x e. { x e. NN | ph } <-> ( x e. NN /\ ph ) )
11 df-ral 
 |-  ( A. y e. { x e. NN | ph } x <_ y <-> A. y ( y e. { x e. NN | ph } -> x <_ y ) )
12 1 elrab 
 |-  ( y e. { x e. NN | ph } <-> ( y e. NN /\ ps ) )
13 12 imbi1i 
 |-  ( ( y e. { x e. NN | ph } -> x <_ y ) <-> ( ( y e. NN /\ ps ) -> x <_ y ) )
14 impexp 
 |-  ( ( ( y e. NN /\ ps ) -> x <_ y ) <-> ( y e. NN -> ( ps -> x <_ y ) ) )
15 13 14 bitri 
 |-  ( ( y e. { x e. NN | ph } -> x <_ y ) <-> ( y e. NN -> ( ps -> x <_ y ) ) )
16 15 albii 
 |-  ( A. y ( y e. { x e. NN | ph } -> x <_ y ) <-> A. y ( y e. NN -> ( ps -> x <_ y ) ) )
17 11 16 bitri 
 |-  ( A. y e. { x e. NN | ph } x <_ y <-> A. y ( y e. NN -> ( ps -> x <_ y ) ) )
18 10 17 anbi12i 
 |-  ( ( x e. { x e. NN | ph } /\ A. y e. { x e. NN | ph } x <_ y ) <-> ( ( x e. NN /\ ph ) /\ A. y ( y e. NN -> ( ps -> x <_ y ) ) ) )
19 18 exbii 
 |-  ( E. x ( x e. { x e. NN | ph } /\ A. y e. { x e. NN | ph } x <_ y ) <-> E. x ( ( x e. NN /\ ph ) /\ A. y ( y e. NN -> ( ps -> x <_ y ) ) ) )
20 df-ral 
 |-  ( A. y e. NN ( ps -> x <_ y ) <-> A. y ( y e. NN -> ( ps -> x <_ y ) ) )
21 20 anbi2i 
 |-  ( ( ( x e. NN /\ ph ) /\ A. y e. NN ( ps -> x <_ y ) ) <-> ( ( x e. NN /\ ph ) /\ A. y ( y e. NN -> ( ps -> x <_ y ) ) ) )
22 anass 
 |-  ( ( ( x e. NN /\ ph ) /\ A. y e. NN ( ps -> x <_ y ) ) <-> ( x e. NN /\ ( ph /\ A. y e. NN ( ps -> x <_ y ) ) ) )
23 21 22 bitr3i 
 |-  ( ( ( x e. NN /\ ph ) /\ A. y ( y e. NN -> ( ps -> x <_ y ) ) ) <-> ( x e. NN /\ ( ph /\ A. y e. NN ( ps -> x <_ y ) ) ) )
24 23 exbii 
 |-  ( E. x ( ( x e. NN /\ ph ) /\ A. y ( y e. NN -> ( ps -> x <_ y ) ) ) <-> E. x ( x e. NN /\ ( ph /\ A. y e. NN ( ps -> x <_ y ) ) ) )
25 df-rex 
 |-  ( E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) <-> E. x ( x e. NN /\ ( ph /\ A. y e. NN ( ps -> x <_ y ) ) ) )
26 24 25 bitr4i 
 |-  ( E. x ( ( x e. NN /\ ph ) /\ A. y ( y e. NN -> ( ps -> x <_ y ) ) ) <-> E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) )
27 9 19 26 3bitri 
 |-  ( E. x e. { x e. NN | ph } A. y e. { x e. NN | ph } x <_ y <-> E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) )
28 4 8 27 3imtr3i 
 |-  ( E. x e. NN ph -> E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) )