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 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹𝑥 )

Proof

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