Metamath Proof Explorer

Theorem noinfepregs

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

		Ref	Expression
	Assertion	noinfepregs	$⊢ \exists x \in ω F (suc x) \notin F (x)$

Proof

Step	Hyp	Ref	Expression
1		noinfepfnregs	$⊢ ({F ↾}_{ω}) Fn ω \to \exists x \in ω ({F ↾}_{ω}) (suc x) \notin ({F ↾}_{ω}) (x)$
2		peano2	$⊢ x \in ω \to suc x \in ω$
3	2	fvresd	$⊢ x \in ω \to ({F ↾}_{ω}) (suc x) = F (suc x)$
4		fvres	$⊢ x \in ω \to ({F ↾}_{ω}) (x) = F (x)$
5	3 4	neleq12d	$⊢ x \in ω \to (({F ↾}_{ω}) (suc x) \notin ({F ↾}_{ω}) (x) \leftrightarrow F (suc x) \notin F (x))$
6	5	rexbiia	$⊢ \exists x \in ω ({F ↾}_{ω}) (suc x) \notin ({F ↾}_{ω}) (x) \leftrightarrow \exists x \in ω F (suc x) \notin F (x)$
7	1 6	sylib	$⊢ ({F ↾}_{ω}) Fn ω \to \exists x \in ω F (suc x) \notin F (x)$
8		fnres	$⊢ ({F ↾}_{ω}) Fn ω \leftrightarrow \forall x \in ω \exists! y x F y$
9	8	notbii	$⊢ \neg ({F ↾}_{ω}) Fn ω \leftrightarrow \neg \forall x \in ω \exists! y x F y$
10		rexnal	$⊢ \exists x \in ω \neg \exists! y x F y \leftrightarrow \neg \forall x \in ω \exists! y x F y$
11	9 10	sylbb2	$⊢ \neg ({F ↾}_{ω}) Fn ω \to \exists x \in ω \neg \exists! y x F y$
12		tz6.12-2	$⊢ \neg \exists! y x F y \to F (x) = \emptyset$
13		nel02	$⊢ F (x) = \emptyset \to \neg F (suc x) \in F (x)$
14		df-nel	$⊢ F (suc x) \notin F (x) \leftrightarrow \neg F (suc x) \in F (x)$
15	13 14	sylibr	$⊢ F (x) = \emptyset \to F (suc x) \notin F (x)$
16	12 15	syl	$⊢ \neg \exists! y x F y \to F (suc x) \notin F (x)$
17	16	reximi	$⊢ \exists x \in ω \neg \exists! y x F y \to \exists x \in ω F (suc x) \notin F (x)$
18	11 17	syl	$⊢ \neg ({F ↾}_{ω}) Fn ω \to \exists x \in ω F (suc x) \notin F (x)$
19	7 18	pm2.61i	$⊢ \exists x \in ω F (suc x) \notin F (x)$