Theorem chninf

Description: There is an infinite number of chains for any infinite alphabet and any relation. For instance, all the singletons of alphabet characters match. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chninf	$$⊢A\notin \mathrm{Fin}\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\notin \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢y\in A\to y\in A$$
2	1	s1chn	$$⊢y\in A\to ⟨“y”⟩\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
3	2	rgen	$$⊢\forall y\in A⟨“y”⟩\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
4		s111	$$⊢\left(y\in A\wedge x\in A\right)\to \left(⟨“y”⟩=⟨“x”⟩\leftrightarrow y=x\right)$$
5	4	biimpd	$$⊢\left(y\in A\wedge x\in A\right)\to \left(⟨“y”⟩=⟨“x”⟩\to y=x\right)$$
6	5	rgen2	$$⊢\forall y\in A\forall x\in A\left(⟨“y”⟩=⟨“x”⟩\to y=x\right)$$
7	3 6	pm3.2i	$$⊢\left(\forall y\in A⟨“y”⟩\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\wedge \forall y\in A\forall x\in A\left(⟨“y”⟩=⟨“x”⟩\to y=x\right)\right)$$
8		eqid	$$⊢\left(y\in A⟼⟨“y”⟩\right)=\left(y\in A⟼⟨“y”⟩\right)$$
9		s1eq	$$⊢y=x\to ⟨“y”⟩=⟨“x”⟩$$
10	8 9	f1mpt	$$⊢\left(y\in A⟼⟨“y”⟩\right):A\underset{1-1}{⟶}{\mathrm{Chain}}_A\underset{\dot{}}{<}\leftrightarrow \left(\forall y\in A⟨“y”⟩\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\wedge \forall y\in A\forall x\in A\left(⟨“y”⟩=⟨“x”⟩\to y=x\right)\right)$$
11	7 10	mpbir	$$⊢\left(y\in A⟼⟨“y”⟩\right):A\underset{1-1}{⟶}{\mathrm{Chain}}_A\underset{\dot{}}{<}$$
12		f1fi	$$⊢\left({\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}\wedge \left(y\in A⟼⟨“y”⟩\right):A\underset{1-1}{⟶}{\mathrm{Chain}}_A\underset{\dot{}}{<}\right)\to A\in \mathrm{Fin}$$
13	11 12	mpan2	$$⊢{\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}\to A\in \mathrm{Fin}$$
14	13	a1i	$$⊢\top \to \left({\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}\to A\in \mathrm{Fin}\right)$$
15	14	nelcon3d	$$⊢\top \to \left(A\notin \mathrm{Fin}\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\notin \mathrm{Fin}\right)$$
16	15	mptru	$$⊢A\notin \mathrm{Fin}\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\notin \mathrm{Fin}$$