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	|- ( .< Po A -> ( A e. Fin <-> ( .< Chain A ) e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		chnfi	|- ( ( A e. Fin /\ .< Po A ) -> ( .< Chain A ) e. Fin )
2	1	expcom	|- ( .< Po A -> ( A e. Fin -> ( .< Chain A ) e. Fin ) )
3		chninf	|- ( A e/ Fin -> ( .< Chain A ) e/ Fin )
4		df-nel	|- ( A e/ Fin <-> -. A e. Fin )
5		df-nel	|- ( ( .< Chain A ) e/ Fin <-> -. ( .< Chain A ) e. Fin )
6	3 4 5	3imtr3i	|- ( -. A e. Fin -> -. ( .< Chain A ) e. Fin )
7	6	con4i	|- ( ( .< Chain A ) e. Fin -> A e. Fin )
8	2 7	impbid1	|- ( .< Po A -> ( A e. Fin <-> ( .< Chain A ) e. Fin ) )