Metamath Proof Explorer

Theorem peano5

Description: The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's five postulates for arithmetic. Proposition 7.30(5) of TakeutiZaring p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction step, is derived from this theorem as Theorem findes . (Contributed by NM, 18-Feb-2004)

Ref Expression
Assertion peano5 
|- ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) -> _om C_ A )

Proof

Step Hyp Ref Expression
1 eldifn 
 |-  ( y e. ( _om \ A ) -> -. y e. A )
2 1 adantl 
 |-  ( ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) /\ y e. ( _om \ A ) ) -> -. y e. A )
3 eldifi 
 |-  ( y e. ( _om \ A ) -> y e. _om )
4 elndif 
 |-  ( (/) e. A -> -. (/) e. ( _om \ A ) )
5 eleq1 
 |-  ( y = (/) -> ( y e. ( _om \ A ) <-> (/) e. ( _om \ A ) ) )
6 5 biimpcd 
 |-  ( y e. ( _om \ A ) -> ( y = (/) -> (/) e. ( _om \ A ) ) )
7 6 necon3bd 
 |-  ( y e. ( _om \ A ) -> ( -. (/) e. ( _om \ A ) -> y =/= (/) ) )
8 4 7 mpan9 
 |-  ( ( (/) e. A /\ y e. ( _om \ A ) ) -> y =/= (/) )
9 nnsuc 
 |-  ( ( y e. _om /\ y =/= (/) ) -> E. x e. _om y = suc x )
10 3 8 9 syl2an2 
 |-  ( ( (/) e. A /\ y e. ( _om \ A ) ) -> E. x e. _om y = suc x )
11 10 ad4ant13 
 |-  ( ( ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) /\ y e. ( _om \ A ) ) /\ ( ( _om \ A ) i^i y ) = (/) ) -> E. x e. _om y = suc x )
12 nfra1 
 |-  F/ x A. x e. _om ( x e. A -> suc x e. A )
13 nfv 
 |-  F/ x ( y e. ( _om \ A ) /\ ( ( _om \ A ) i^i y ) = (/) )
14 12 13 nfan 
 |-  F/ x ( A. x e. _om ( x e. A -> suc x e. A ) /\ ( y e. ( _om \ A ) /\ ( ( _om \ A ) i^i y ) = (/) ) )
15 nfv 
 |-  F/ x y e. A
16 rsp 
 |-  ( A. x e. _om ( x e. A -> suc x e. A ) -> ( x e. _om -> ( x e. A -> suc x e. A ) ) )
17 vex 
 |-  x e. _V
18 17 sucid 
 |-  x e. suc x
19 eleq2 
 |-  ( y = suc x -> ( x e. y <-> x e. suc x ) )
20 18 19 mpbiri 
 |-  ( y = suc x -> x e. y )
21 eleq1 
 |-  ( y = suc x -> ( y e. _om <-> suc x e. _om ) )
22 peano2b 
 |-  ( x e. _om <-> suc x e. _om )
23 21 22 bitr4di 
 |-  ( y = suc x -> ( y e. _om <-> x e. _om ) )
24 minel 
 |-  ( ( x e. y /\ ( ( _om \ A ) i^i y ) = (/) ) -> -. x e. ( _om \ A ) )
25 neldif 
 |-  ( ( x e. _om /\ -. x e. ( _om \ A ) ) -> x e. A )
26 24 25 sylan2 
 |-  ( ( x e. _om /\ ( x e. y /\ ( ( _om \ A ) i^i y ) = (/) ) ) -> x e. A )
27 26 exp32 
 |-  ( x e. _om -> ( x e. y -> ( ( ( _om \ A ) i^i y ) = (/) -> x e. A ) ) )
28 23 27 syl6bi 
 |-  ( y = suc x -> ( y e. _om -> ( x e. y -> ( ( ( _om \ A ) i^i y ) = (/) -> x e. A ) ) ) )
29 20 28 mpid 
 |-  ( y = suc x -> ( y e. _om -> ( ( ( _om \ A ) i^i y ) = (/) -> x e. A ) ) )
30 3 29 syl5 
 |-  ( y = suc x -> ( y e. ( _om \ A ) -> ( ( ( _om \ A ) i^i y ) = (/) -> x e. A ) ) )
31 30 impd 
 |-  ( y = suc x -> ( ( y e. ( _om \ A ) /\ ( ( _om \ A ) i^i y ) = (/) ) -> x e. A ) )
32 eleq1a 
 |-  ( suc x e. A -> ( y = suc x -> y e. A ) )
33 32 com12 
 |-  ( y = suc x -> ( suc x e. A -> y e. A ) )
34 31 33 imim12d 
 |-  ( y = suc x -> ( ( x e. A -> suc x e. A ) -> ( ( y e. ( _om \ A ) /\ ( ( _om \ A ) i^i y ) = (/) ) -> y e. A ) ) )
35 34 com13 
 |-  ( ( y e. ( _om \ A ) /\ ( ( _om \ A ) i^i y ) = (/) ) -> ( ( x e. A -> suc x e. A ) -> ( y = suc x -> y e. A ) ) )
36 16 35 sylan9 
 |-  ( ( A. x e. _om ( x e. A -> suc x e. A ) /\ ( y e. ( _om \ A ) /\ ( ( _om \ A ) i^i y ) = (/) ) ) -> ( x e. _om -> ( y = suc x -> y e. A ) ) )
37 14 15 36 rexlimd 
 |-  ( ( A. x e. _om ( x e. A -> suc x e. A ) /\ ( y e. ( _om \ A ) /\ ( ( _om \ A ) i^i y ) = (/) ) ) -> ( E. x e. _om y = suc x -> y e. A ) )
38 37 exp32 
 |-  ( A. x e. _om ( x e. A -> suc x e. A ) -> ( y e. ( _om \ A ) -> ( ( ( _om \ A ) i^i y ) = (/) -> ( E. x e. _om y = suc x -> y e. A ) ) ) )
39 38 a1i 
 |-  ( (/) e. A -> ( A. x e. _om ( x e. A -> suc x e. A ) -> ( y e. ( _om \ A ) -> ( ( ( _om \ A ) i^i y ) = (/) -> ( E. x e. _om y = suc x -> y e. A ) ) ) ) )
40 39 imp41 
 |-  ( ( ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) /\ y e. ( _om \ A ) ) /\ ( ( _om \ A ) i^i y ) = (/) ) -> ( E. x e. _om y = suc x -> y e. A ) )
41 11 40 mpd 
 |-  ( ( ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) /\ y e. ( _om \ A ) ) /\ ( ( _om \ A ) i^i y ) = (/) ) -> y e. A )
42 2 41 mtand 
 |-  ( ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) /\ y e. ( _om \ A ) ) -> -. ( ( _om \ A ) i^i y ) = (/) )
43 42 nrexdv 
 |-  ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) -> -. E. y e. ( _om \ A ) ( ( _om \ A ) i^i y ) = (/) )
44 ordom 
 |-  Ord _om
45 difss 
 |-  ( _om \ A ) C_ _om
46 tz7.5 
 |-  ( ( Ord _om /\ ( _om \ A ) C_ _om /\ ( _om \ A ) =/= (/) ) -> E. y e. ( _om \ A ) ( ( _om \ A ) i^i y ) = (/) )
47 44 45 46 mp3an12 
 |-  ( ( _om \ A ) =/= (/) -> E. y e. ( _om \ A ) ( ( _om \ A ) i^i y ) = (/) )
48 47 necon1bi 
 |-  ( -. E. y e. ( _om \ A ) ( ( _om \ A ) i^i y ) = (/) -> ( _om \ A ) = (/) )
49 43 48 syl 
 |-  ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) -> ( _om \ A ) = (/) )
50 ssdif0 
 |-  ( _om C_ A <-> ( _om \ A ) = (/) )
51 49 50 sylibr 
 |-  ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) -> _om C_ A )