Theorem chnfi

Description: There is a finite number of chains over finite domain, as long as the relation orders it. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chnfi	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → ( < Chain 𝐴 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		iunrab	⊢ ∪ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } = { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑥 ) = 𝑛 }
2		simplr	⊢ ( ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) ∧ 𝑥 ∈ ( < Chain 𝐴 ) ) → < Po 𝐴 )
3		simpr	⊢ ( ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) ∧ 𝑥 ∈ ( < Chain 𝐴 ) ) → 𝑥 ∈ ( < Chain 𝐴 ) )
4		simpll	⊢ ( ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) ∧ 𝑥 ∈ ( < Chain 𝐴 ) ) → 𝐴 ∈ Fin )
5	2 3 4	chnpolfz	⊢ ( ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) ∧ 𝑥 ∈ ( < Chain 𝐴 ) ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
6		risset	⊢ ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) 𝑛 = ( ♯ ‘ 𝑥 ) )
7		eqcom	⊢ ( 𝑛 = ( ♯ ‘ 𝑥 ) ↔ ( ♯ ‘ 𝑥 ) = 𝑛 )
8	7	rexbii	⊢ ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) 𝑛 = ( ♯ ‘ 𝑥 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑥 ) = 𝑛 )
9	6 8	bitri	⊢ ( ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑥 ) = 𝑛 )
10	5 9	sylib	⊢ ( ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) ∧ 𝑥 ∈ ( < Chain 𝐴 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑥 ) = 𝑛 )
11	10	rabeqcda	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( ♯ ‘ 𝑥 ) = 𝑛 } = ( < Chain 𝐴 ) )
12	1 11	eqtr2id	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → ( < Chain 𝐴 ) = ∪ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } )
13		fzfid	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → ( 0 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin )
14		chnflenfi	⊢ ( 𝐴 ∈ Fin → { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } ∈ Fin )
15	14	adantr	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } ∈ Fin )
16	15	ralrimivw	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } ∈ Fin )
17		iunfi	⊢ ( ( ( 0 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin ∧ ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } ∈ Fin ) → ∪ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } ∈ Fin )
18	13 16 17	syl2anc	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → ∪ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) { 𝑥 ∈ ( < Chain 𝐴 ) ∣ ( ♯ ‘ 𝑥 ) = 𝑛 } ∈ Fin )
19	12 18	eqeltrd	⊢ ( ( 𝐴 ∈ Fin ∧ < Po 𝐴 ) → ( < Chain 𝐴 ) ∈ Fin )