Metamath Proof Explorer

Theorem noinfep

Description: Using the Axiom of Regularity in the form zfregfr , show that there are no infinite descending e. -chains. Proposition 7.34 of TakeutiZaring p. 44. (Contributed by NM, 26-Jan-2006) (Revised by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion noinfep 
|- E. x e. _om ( F ` suc x ) e/ ( F ` x )

Proof

Step Hyp Ref Expression
1 omex 
 |-  _om e. _V
2 1 mptex 
 |-  ( w e. _om |-> ( F ` w ) ) e. _V
3 2 rnex 
 |-  ran ( w e. _om |-> ( F ` w ) ) e. _V
4 zfregfr 
 |-  _E Fr ran ( w e. _om |-> ( F ` w ) )
5 ssid 
 |-  ran ( w e. _om |-> ( F ` w ) ) C_ ran ( w e. _om |-> ( F ` w ) )
6 dmmptg 
 |-  ( A. w e. _om ( F ` w ) e. _V -> dom ( w e. _om |-> ( F ` w ) ) = _om )
7 fvexd 
 |-  ( w e. _om -> ( F ` w ) e. _V )
8 6 7 mprg 
 |-  dom ( w e. _om |-> ( F ` w ) ) = _om
9 peano1 
 |-  (/) e. _om
10 9 ne0ii 
 |-  _om =/= (/)
11 8 10 eqnetri 
 |-  dom ( w e. _om |-> ( F ` w ) ) =/= (/)
12 dm0rn0 
 |-  ( dom ( w e. _om |-> ( F ` w ) ) = (/) <-> ran ( w e. _om |-> ( F ` w ) ) = (/) )
13 12 necon3bii 
 |-  ( dom ( w e. _om |-> ( F ` w ) ) =/= (/) <-> ran ( w e. _om |-> ( F ` w ) ) =/= (/) )
14 11 13 mpbi 
 |-  ran ( w e. _om |-> ( F ` w ) ) =/= (/)
15 fri 
 |-  ( ( ( ran ( w e. _om |-> ( F ` w ) ) e. _V /\ _E Fr ran ( w e. _om |-> ( F ` w ) ) ) /\ ( ran ( w e. _om |-> ( F ` w ) ) C_ ran ( w e. _om |-> ( F ` w ) ) /\ ran ( w e. _om |-> ( F ` w ) ) =/= (/) ) ) -> E. y e. ran ( w e. _om |-> ( F ` w ) ) A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y )
16 3 4 5 14 15 mp4an 
 |-  E. y e. ran ( w e. _om |-> ( F ` w ) ) A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y
17 fvex 
 |-  ( F ` w ) e. _V
18 eqid 
 |-  ( w e. _om |-> ( F ` w ) ) = ( w e. _om |-> ( F ` w ) )
19 17 18 fnmpti 
 |-  ( w e. _om |-> ( F ` w ) ) Fn _om
20 fvelrnb 
 |-  ( ( w e. _om |-> ( F ` w ) ) Fn _om -> ( y e. ran ( w e. _om |-> ( F ` w ) ) <-> E. x e. _om ( ( w e. _om |-> ( F ` w ) ) ` x ) = y ) )
21 19 20 ax-mp 
 |-  ( y e. ran ( w e. _om |-> ( F ` w ) ) <-> E. x e. _om ( ( w e. _om |-> ( F ` w ) ) ` x ) = y )
22 peano2 
 |-  ( x e. _om -> suc x e. _om )
23 fveq2 
 |-  ( w = suc x -> ( F ` w ) = ( F ` suc x ) )
24 fvex 
 |-  ( F ` suc x ) e. _V
25 23 18 24 fvmpt 
 |-  ( suc x e. _om -> ( ( w e. _om |-> ( F ` w ) ) ` suc x ) = ( F ` suc x ) )
26 22 25 syl 
 |-  ( x e. _om -> ( ( w e. _om |-> ( F ` w ) ) ` suc x ) = ( F ` suc x ) )
27 fnfvelrn 
 |-  ( ( ( w e. _om |-> ( F ` w ) ) Fn _om /\ suc x e. _om ) -> ( ( w e. _om |-> ( F ` w ) ) ` suc x ) e. ran ( w e. _om |-> ( F ` w ) ) )
28 19 22 27 sylancr 
 |-  ( x e. _om -> ( ( w e. _om |-> ( F ` w ) ) ` suc x ) e. ran ( w e. _om |-> ( F ` w ) ) )
29 26 28 eqeltrrd 
 |-  ( x e. _om -> ( F ` suc x ) e. ran ( w e. _om |-> ( F ` w ) ) )
30 epel 
 |-  ( z _E y <-> z e. y )
31 eleq1 
 |-  ( z = ( F ` suc x ) -> ( z e. y <-> ( F ` suc x ) e. y ) )
32 30 31 bitrid 
 |-  ( z = ( F ` suc x ) -> ( z _E y <-> ( F ` suc x ) e. y ) )
33 32 notbid 
 |-  ( z = ( F ` suc x ) -> ( -. z _E y <-> -. ( F ` suc x ) e. y ) )
34 df-nel 
 |-  ( ( F ` suc x ) e/ y <-> -. ( F ` suc x ) e. y )
35 33 34 bitr4di 
 |-  ( z = ( F ` suc x ) -> ( -. z _E y <-> ( F ` suc x ) e/ y ) )
36 35 rspccv 
 |-  ( A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y -> ( ( F ` suc x ) e. ran ( w e. _om |-> ( F ` w ) ) -> ( F ` suc x ) e/ y ) )
37 29 36 syl5com 
 |-  ( x e. _om -> ( A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y -> ( F ` suc x ) e/ y ) )
38 fveq2 
 |-  ( w = x -> ( F ` w ) = ( F ` x ) )
39 fvex 
 |-  ( F ` x ) e. _V
40 38 18 39 fvmpt 
 |-  ( x e. _om -> ( ( w e. _om |-> ( F ` w ) ) ` x ) = ( F ` x ) )
41 eqeq1 
 |-  ( ( ( w e. _om |-> ( F ` w ) ) ` x ) = y -> ( ( ( w e. _om |-> ( F ` w ) ) ` x ) = ( F ` x ) <-> y = ( F ` x ) ) )
42 40 41 syl5ibcom 
 |-  ( x e. _om -> ( ( ( w e. _om |-> ( F ` w ) ) ` x ) = y -> y = ( F ` x ) ) )
43 neleq2 
 |-  ( y = ( F ` x ) -> ( ( F ` suc x ) e/ y <-> ( F ` suc x ) e/ ( F ` x ) ) )
44 43 biimpd 
 |-  ( y = ( F ` x ) -> ( ( F ` suc x ) e/ y -> ( F ` suc x ) e/ ( F ` x ) ) )
45 42 44 syl6 
 |-  ( x e. _om -> ( ( ( w e. _om |-> ( F ` w ) ) ` x ) = y -> ( ( F ` suc x ) e/ y -> ( F ` suc x ) e/ ( F ` x ) ) ) )
46 45 com23 
 |-  ( x e. _om -> ( ( F ` suc x ) e/ y -> ( ( ( w e. _om |-> ( F ` w ) ) ` x ) = y -> ( F ` suc x ) e/ ( F ` x ) ) ) )
47 37 46 syldc 
 |-  ( A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y -> ( x e. _om -> ( ( ( w e. _om |-> ( F ` w ) ) ` x ) = y -> ( F ` suc x ) e/ ( F ` x ) ) ) )
48 47 reximdvai 
 |-  ( A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y -> ( E. x e. _om ( ( w e. _om |-> ( F ` w ) ) ` x ) = y -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) ) )
49 21 48 syl5bi 
 |-  ( A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y -> ( y e. ran ( w e. _om |-> ( F ` w ) ) -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) ) )
50 49 com12 
 |-  ( y e. ran ( w e. _om |-> ( F ` w ) ) -> ( A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) ) )
51 50 rexlimiv 
 |-  ( E. y e. ran ( w e. _om |-> ( F ` w ) ) A. z e. ran ( w e. _om |-> ( F ` w ) ) -. z _E y -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )
52 16 51 ax-mp 
 |-  E. x e. _om ( F ` suc x ) e/ ( F ` x )