Theorem noinfepregs

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

	Ref	Expression
Assertion	noinfepregs	|- E. x e. _om ( F ` suc x ) e/ ( F ` x )

Proof

Step	Hyp	Ref	Expression
1		noinfepfnregs	|- ( ( F |` _om ) Fn _om -> E. x e. _om ( ( F |` _om ) ` suc x ) e/ ( ( F |` _om ) ` x ) )
2		peano2	|- ( x e. _om -> suc x e. _om )
3	2	fvresd	|- ( x e. _om -> ( ( F |` _om ) ` suc x ) = ( F ` suc x ) )
4		fvres	|- ( x e. _om -> ( ( F |` _om ) ` x ) = ( F ` x ) )
5	3 4	neleq12d	|- ( x e. _om -> ( ( ( F |` _om ) ` suc x ) e/ ( ( F |` _om ) ` x ) <-> ( F ` suc x ) e/ ( F ` x ) ) )
6	5	rexbiia	|- ( E. x e. _om ( ( F |` _om ) ` suc x ) e/ ( ( F |` _om ) ` x ) <-> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )
7	1 6	sylib	|- ( ( F |` _om ) Fn _om -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )
8		fnres	|- ( ( F |` _om ) Fn _om <-> A. x e. _om E! y x F y )
9	8	notbii	|- ( -. ( F |` _om ) Fn _om <-> -. A. x e. _om E! y x F y )
10		rexnal	|- ( E. x e. _om -. E! y x F y <-> -. A. x e. _om E! y x F y )
11	9 10	sylbb2	|- ( -. ( F |` _om ) Fn _om -> E. x e. _om -. E! y x F y )
12		tz6.12-2	|- ( -. E! y x F y -> ( F ` x ) = (/) )
13		nel02	|- ( ( F ` x ) = (/) -> -. ( F ` suc x ) e. ( F ` x ) )
14		df-nel	|- ( ( F ` suc x ) e/ ( F ` x ) <-> -. ( F ` suc x ) e. ( F ` x ) )
15	13 14	sylibr	|- ( ( F ` x ) = (/) -> ( F ` suc x ) e/ ( F ` x ) )
16	12 15	syl	|- ( -. E! y x F y -> ( F ` suc x ) e/ ( F ` x ) )
17	16	reximi	|- ( E. x e. _om -. E! y x F y -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )
18	11 17	syl	|- ( -. ( F |` _om ) Fn _om -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )
19	7 18	pm2.61i	|- E. x e. _om ( F ` suc x ) e/ ( F ` x )