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 bitrid ⊢ ( 𝑧 = ( 𝐹 ‘ 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 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 )