Metamath Proof Explorer

Theorem peano5nni

Description: Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of Apostol p. 34. (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion peano5nni 
|- ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> NN C_ A )

Proof

Step Hyp Ref Expression
1 df-nn 
 |-  NN = ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) " _om )
2 df-ima 
 |-  ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) " _om ) = ran ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om )
3 1 2 eqtri 
 |-  NN = ran ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om )
4 frfnom 
 |-  ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) Fn _om
5 4 a1i 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) Fn _om )
6 fveq2 
 |-  ( y = (/) -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` (/) ) )
7 6 eleq1d 
 |-  ( y = (/) -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` (/) ) e. A ) )
8 fveq2 
 |-  ( y = z -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) )
9 8 eleq1d 
 |-  ( y = z -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) e. A ) )
10 fveq2 
 |-  ( y = suc z -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) )
11 10 eleq1d 
 |-  ( y = suc z -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) e. A ) )
12 ax-1cn 
 |-  1 e. CC
13 fr0g 
 |-  ( 1 e. CC -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` (/) ) = 1 )
14 12 13 ax-mp 
 |-  ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` (/) ) = 1
15 simpl 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> 1 e. A )
16 14 15 eqeltrid 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` (/) ) e. A )
17 oveq1 
 |-  ( x = ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) -> ( x + 1 ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) )
18 17 eleq1d 
 |-  ( x = ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) -> ( ( x + 1 ) e. A <-> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) e. A ) )
19 18 rspccv 
 |-  ( A. x e. A ( x + 1 ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) e. A ) )
20 19 ad2antlr 
 |-  ( ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) /\ z e. _om ) -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) e. A ) )
21 ovex 
 |-  ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) e. _V
22 eqid 
 |-  ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) = ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om )
23 oveq1 
 |-  ( y = n -> ( y + 1 ) = ( n + 1 ) )
24 oveq1 
 |-  ( y = ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) -> ( y + 1 ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) )
25 22 23 24 frsucmpt2 
 |-  ( ( z e. _om /\ ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) e. _V ) -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) )
26 21 25 mpan2 
 |-  ( z e. _om -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) = ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) )
27 26 eleq1d 
 |-  ( z e. _om -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) e. A <-> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) e. A ) )
28 27 adantl 
 |-  ( ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) /\ z e. _om ) -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) e. A <-> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) + 1 ) e. A ) )
29 20 28 sylibrd 
 |-  ( ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) /\ z e. _om ) -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) e. A -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) e. A ) )
30 29 expcom 
 |-  ( z e. _om -> ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> ( ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` z ) e. A -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` suc z ) e. A ) ) )
31 7 9 11 16 30 finds2 
 |-  ( y e. _om -> ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) e. A ) )
32 31 com12 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> ( y e. _om -> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) e. A ) )
33 32 ralrimiv 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> A. y e. _om ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) e. A )
34 ffnfv 
 |-  ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) : _om --> A <-> ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) Fn _om /\ A. y e. _om ( ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) ` y ) e. A ) )
35 5 33 34 sylanbrc 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) : _om --> A )
36 35 frnd 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> ran ( rec ( ( n e. _V |-> ( n + 1 ) ) , 1 ) |` _om ) C_ A )
37 3 36 eqsstrid 
 |-  ( ( 1 e. A /\ A. x e. A ( x + 1 ) e. A ) -> NN C_ A )