Metamath Proof Explorer

Theorem peano5OLD

Description: Obsolete version of peano5 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion peano5OLD 
|- ( ( (/) 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 )