Theorem chnfibg

Description: Given a partial order, the set of chains is finite iff the alphabet is finite. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chnfibg	$$⊢\underset{\dot{}}{<}\mathrm{Po}A\to \left(A\in \mathrm{Fin}\leftrightarrow {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		chnfi	$$⊢\left(A\in \mathrm{Fin}\wedge \underset{\dot{}}{<}\mathrm{Po}A\right)\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}$$
2	1	expcom	$$⊢\underset{\dot{}}{<}\mathrm{Po}A\to \left(A\in \mathrm{Fin}\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}\right)$$
3		chninf	$$⊢A\notin \mathrm{Fin}\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\notin \mathrm{Fin}$$
4		df-nel	$$⊢A\notin \mathrm{Fin}\leftrightarrow \neg A\in \mathrm{Fin}$$
5		df-nel	$$⊢{\mathrm{Chain}}_A\underset{\dot{}}{<}\notin \mathrm{Fin}\leftrightarrow \neg {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}$$
6	3 4 5	3imtr3i	$$⊢\neg A\in \mathrm{Fin}\to \neg {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}$$
7	6	con4i	$$⊢{\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}\to A\in \mathrm{Fin}$$
8	2 7	impbid1	$$⊢\underset{\dot{}}{<}\mathrm{Po}A\to \left(A\in \mathrm{Fin}\leftrightarrow {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{Fin}\right)$$