Theorem noinfepregs

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

	Ref	Expression
Assertion	noinfepregs	⊢ ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		noinfepfnregs	⊢ ( ( 𝐹 ↾ ω ) Fn ω → ∃ 𝑥 ∈ ω ( ( 𝐹 ↾ ω ) ‘ suc 𝑥 ) ∉ ( ( 𝐹 ↾ ω ) ‘ 𝑥 ) )
2		peano2	⊢ ( 𝑥 ∈ ω → suc 𝑥 ∈ ω )
3	2	fvresd	⊢ ( 𝑥 ∈ ω → ( ( 𝐹 ↾ ω ) ‘ suc 𝑥 ) = ( 𝐹 ‘ suc 𝑥 ) )
4		fvres	⊢ ( 𝑥 ∈ ω → ( ( 𝐹 ↾ ω ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
5	3 4	neleq12d	⊢ ( 𝑥 ∈ ω → ( ( ( 𝐹 ↾ ω ) ‘ suc 𝑥 ) ∉ ( ( 𝐹 ↾ ω ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ) )
6	5	rexbiia	⊢ ( ∃ 𝑥 ∈ ω ( ( 𝐹 ↾ ω ) ‘ suc 𝑥 ) ∉ ( ( 𝐹 ↾ ω ) ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
7	1 6	sylib	⊢ ( ( 𝐹 ↾ ω ) Fn ω → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
8		fnres	⊢ ( ( 𝐹 ↾ ω ) Fn ω ↔ ∀ 𝑥 ∈ ω ∃! 𝑦 𝑥 𝐹 𝑦 )
9	8	notbii	⊢ ( ¬ ( 𝐹 ↾ ω ) Fn ω ↔ ¬ ∀ 𝑥 ∈ ω ∃! 𝑦 𝑥 𝐹 𝑦 )
10		rexnal	⊢ ( ∃ 𝑥 ∈ ω ¬ ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ¬ ∀ 𝑥 ∈ ω ∃! 𝑦 𝑥 𝐹 𝑦 )
11	9 10	sylbb2	⊢ ( ¬ ( 𝐹 ↾ ω ) Fn ω → ∃ 𝑥 ∈ ω ¬ ∃! 𝑦 𝑥 𝐹 𝑦 )
12		tz6.12-2	⊢ ( ¬ ∃! 𝑦 𝑥 𝐹 𝑦 → ( 𝐹 ‘ 𝑥 ) = ∅ )
13		nel02	⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
14		df-nel	⊢ ( ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
15	13 14	sylibr	⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
16	12 15	syl	⊢ ( ¬ ∃! 𝑦 𝑥 𝐹 𝑦 → ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
17	16	reximi	⊢ ( ∃ 𝑥 ∈ ω ¬ ∃! 𝑦 𝑥 𝐹 𝑦 → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
18	11 17	syl	⊢ ( ¬ ( 𝐹 ↾ ω ) Fn ω → ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 ) )
19	7 18	pm2.61i	⊢ ∃ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∉ ( 𝐹 ‘ 𝑥 )