noinfepfnregs

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

		Ref	Expression
	Assertion	noinfepfnregs	$⊢ F Fn ω \to \exists x \in ω F (suc x) \notin F (x)$

Proof

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2	1	n0ii	$⊢ \neg ω = \emptyset$
3		ssid	$⊢ ω \subseteq ω$
4		fnimaeq0	$⊢ (F Fn ω \land ω \subseteq ω) \to (F [ω] = \emptyset \leftrightarrow ω = \emptyset)$
5	3 4	mpan2	$⊢ F Fn ω \to (F [ω] = \emptyset \leftrightarrow ω = \emptyset)$
6	2 5	mtbiri	$⊢ F Fn ω \to \neg F [ω] = \emptyset$
7	6	neqned	$⊢ F Fn ω \to F [ω] \neq \emptyset$
8		axregszf	$⊢ F [ω] \neq \emptyset \to \exists y \in F [ω] y \cap F [ω] = \emptyset$
9	7 8	syl	$⊢ F Fn ω \to \exists y \in F [ω] y \cap F [ω] = \emptyset$
10		fvelimab	$⊢ (F Fn ω \land ω \subseteq ω) \to (y \in F [ω] \leftrightarrow \exists x \in ω F (x) = y)$
11	3 10	mpan2	$⊢ F Fn ω \to (y \in F [ω] \leftrightarrow \exists x \in ω F (x) = y)$
12	11	adantr	$⊢ (F Fn ω \land y \cap F [ω] = \emptyset) \to (y \in F [ω] \leftrightarrow \exists x \in ω F (x) = y)$
13		simprl	$⊢ ((F Fn ω \land y \cap F [ω] = \emptyset) \land (x \in ω \land F (x) = y)) \to x \in ω$
14		peano2	$⊢ x \in ω \to suc x \in ω$
15		fnfvima	$⊢ (F Fn ω \land ω \subseteq ω \land suc x \in ω) \to F (suc x) \in F [ω]$
16	3 15	mp3an2	$⊢ (F Fn ω \land suc x \in ω) \to F (suc x) \in F [ω]$
17	14 16	sylan2	$⊢ (F Fn ω \land x \in ω) \to F (suc x) \in F [ω]$
18	17	ad2ant2r	$⊢ ((F Fn ω \land y \cap F [ω] = \emptyset) \land (x \in ω \land F (x) = y)) \to F (suc x) \in F [ω]$
19		ineq1	$⊢ F (x) = y \to F (x) \cap F [ω] = y \cap F [ω]$
20	19	eqeq1d	$⊢ F (x) = y \to (F (x) \cap F [ω] = \emptyset \leftrightarrow y \cap F [ω] = \emptyset)$
21	20	biimparc	$⊢ (y \cap F [ω] = \emptyset \land F (x) = y) \to F (x) \cap F [ω] = \emptyset$
22	21	ad2ant2l	$⊢ ((F Fn ω \land y \cap F [ω] = \emptyset) \land (x \in ω \land F (x) = y)) \to F (x) \cap F [ω] = \emptyset$
23		minel	$⊢ (F (suc x) \in F [ω] \land F (x) \cap F [ω] = \emptyset) \to \neg F (suc x) \in F (x)$
24	18 22 23	syl2anc	$⊢ ((F Fn ω \land y \cap F [ω] = \emptyset) \land (x \in ω \land F (x) = y)) \to \neg F (suc x) \in F (x)$
25		df-nel	$⊢ F (suc x) \notin F (x) \leftrightarrow \neg F (suc x) \in F (x)$
26	24 25	sylibr	$⊢ ((F Fn ω \land y \cap F [ω] = \emptyset) \land (x \in ω \land F (x) = y)) \to F (suc x) \notin F (x)$
27	13 26	jca	$⊢ ((F Fn ω \land y \cap F [ω] = \emptyset) \land (x \in ω \land F (x) = y)) \to (x \in ω \land F (suc x) \notin F (x))$
28	27	ex	$⊢ (F Fn ω \land y \cap F [ω] = \emptyset) \to ((x \in ω \land F (x) = y) \to (x \in ω \land F (suc x) \notin F (x)))$
29	28	reximdv2	$⊢ (F Fn ω \land y \cap F [ω] = \emptyset) \to (\exists x \in ω F (x) = y \to \exists x \in ω F (suc x) \notin F (x))$
30	12 29	sylbid	$⊢ (F Fn ω \land y \cap F [ω] = \emptyset) \to (y \in F [ω] \to \exists x \in ω F (suc x) \notin F (x))$
31	30	expimpd	$⊢ F Fn ω \to ((y \cap F [ω] = \emptyset \land y \in F [ω]) \to \exists x \in ω F (suc x) \notin F (x))$
32	31	ancomsd	$⊢ F Fn ω \to ((y \in F [ω] \land y \cap F [ω] = \emptyset) \to \exists x \in ω F (suc x) \notin F (x))$
33	32	imp	$⊢ (F Fn ω \land (y \in F [ω] \land y \cap F [ω] = \emptyset)) \to \exists x \in ω F (suc x) \notin F (x)$
34	9 33	rexlimddv	$⊢ F Fn ω \to \exists x \in ω F (suc x) \notin F (x)$

Metamath Proof Explorer

Theorem noinfepfnregs

Proof