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 𝐴 → ( 𝐴 ∈ Fin ↔ ( < Chain 𝐴 ) ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		chnfi	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → ( < Chain 𝐴 ) ∈ Fin )
2	1	expcom	⊢ ( < Po 𝐴 → ( 𝐴 ∈ Fin → ( < Chain 𝐴 ) ∈ Fin ) )
3		chninf	⊢ ( 𝐴 ∉ Fin → ( < Chain 𝐴 ) ∉ Fin )
4		df-nel	⊢ ( 𝐴 ∉ Fin ↔ ¬ 𝐴 ∈ Fin )
5		df-nel	⊢ ( ( < Chain 𝐴 ) ∉ Fin ↔ ¬ ( < Chain 𝐴 ) ∈ Fin )
6	3 4 5	3imtr3i	⊢ ( ¬ 𝐴 ∈ Fin → ¬ ( < Chain 𝐴 ) ∈ Fin )
7	6	con4i	⊢ ( ( < Chain 𝐴 ) ∈ Fin → 𝐴 ∈ Fin )
8	2 7	impbid1	⊢ ( < Po 𝐴 → ( 𝐴 ∈ Fin ↔ ( < Chain 𝐴 ) ∈ Fin ) )