Metamath Proof Explorer

Theorem noinfepfnregs

Description: There are no infinite descending e. -chains, proven using ax-regs . (Contributed by BTernaryTau, 18-Feb-2026)

Ref Expression
Assertion noinfepfnregs ( 𝐹 Fn ω → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 peano1 ⊢ ∅ ∈ ω
2 1 n0ii ⊢ ¬ ω = ∅
3 ssid ⊢ ω ⊆ ω
4 fnimaeq0 ⊢ ( ( 𝐹 Fn ω ∧ ω ⊆ ω ) → ( ( 𝐹 “ ω ) = ∅ ↔ ω = ∅ ) )
5 3 4 mpan2 ⊢ ( 𝐹 Fn ω → ( ( 𝐹 “ ω ) = ∅ ↔ ω = ∅ ) )
6 2 5 mtbiri ⊢ ( 𝐹 Fn ω → ¬ ( 𝐹 “ ω ) = ∅ )
7 6 neqned ⊢ ( 𝐹 Fn ω → ( 𝐹 “ ω ) ≠ ∅ )
8 axregszf ⊢ ( ( 𝐹 “ ω ) ≠ ∅ → ∃ 𝑦 ∈ ( 𝐹 “ ω ) ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ )
9 7 8 syl ⊢ ( 𝐹 Fn ω → ∃ 𝑦 ∈ ( 𝐹 “ ω ) ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ )
10 fvelimab ⊢ ( ( 𝐹 Fn ω ∧ ω ⊆ ω ) → ( 𝑦 ∈ ( 𝐹 “ ω ) ↔ ∃ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
11 3 10 mpan2 ⊢ ( 𝐹 Fn ω → ( 𝑦 ∈ ( 𝐹 “ ω ) ↔ ∃ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
12 11 adantr ⊢ ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) → ( 𝑦 ∈ ( 𝐹 “ ω ) ↔ ∃ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
13 simprl ⊢ ( ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) → 𝑥 ∈ ω )
14 peano2 ⊢ ( 𝑥 ∈ ω → suc 𝑥 ∈ ω )
15 fnfvima ⊢ ( ( 𝐹 Fn ω ∧ ω ⊆ ω ∧ suc 𝑥 ∈ ω ) → ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 “ ω ) )
16 3 15 mp3an2 ⊢ ( ( 𝐹 Fn ω ∧ suc 𝑥 ∈ ω ) → ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 “ ω ) )
17 14 16 sylan2 ⊢ ( ( 𝐹 Fn ω ∧ 𝑥 ∈ ω ) → ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 “ ω ) )
18 17 ad2ant2r ⊢ ( ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) → ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 “ ω ) )
19 ineq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∩ ( 𝐹 “ ω ) ) = ( 𝑦 ∩ ( 𝐹 “ ω ) ) )
20 19 eqeq1d ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ ( 𝐹 “ ω ) ) = ∅ ↔ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) )
21 20 biimparc ⊢ ( ( ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ ( 𝐹 “ ω ) ) = ∅ )
22 21 ad2ant2l ⊢ ( ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ ( 𝐹 “ ω ) ) = ∅ )
23 minel ⊢ ( ( ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 “ ω ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∩ ( 𝐹 “ ω ) ) = ∅ ) → ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
24 18 22 23 syl2anc ⊢ ( ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) → ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
25 df-nel ⊢ ( ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
26 24 25 sylibr ⊢ ( ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) → ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
27 13 26 jca ⊢ ( ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) ∧ ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) → ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ) )
28 27 ex ⊢ ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) → ( ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ ω ∧ ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ) ) )
29 28 reximdv2 ⊢ ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) → ( ∃ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ) )
30 12 29 sylbid ⊢ ( ( 𝐹 Fn ω ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) → ( 𝑦 ∈ ( 𝐹 “ ω ) → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ) )
31 30 expimpd ⊢ ( 𝐹 Fn ω → ( ( ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ∧ 𝑦 ∈ ( 𝐹 “ ω ) ) → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ) )
32 31 ancomsd ⊢ ( 𝐹 Fn ω → ( ( 𝑦 ∈ ( 𝐹 “ ω ) ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ) )
33 32 imp ⊢ ( ( 𝐹 Fn ω ∧ ( 𝑦 ∈ ( 𝐹 “ ω ) ∧ ( 𝑦 ∩ ( 𝐹 “ ω ) ) = ∅ ) ) → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
34 9 33 rexlimddv ⊢ ( 𝐹 Fn ω → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )