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 x ω F suc x F x

Proof

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