Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 iunrab 
 |-  U_ n e. ( 0 ... ( # ` A ) ) { x e. ( .< Chain A ) | ( # ` x ) = n } = { x e. ( .< Chain A ) | E. n e. ( 0 ... ( # ` A ) ) ( # ` x ) = n }
2 simplr 
 |-  ( ( ( A e. Fin /\ .< Po A ) /\ x e. ( .< Chain A ) ) -> .< Po A )
3 simpr 
 |-  ( ( ( A e. Fin /\ .< Po A ) /\ x e. ( .< Chain A ) ) -> x e. ( .< Chain A ) )
4 simpll 
 |-  ( ( ( A e. Fin /\ .< Po A ) /\ x e. ( .< Chain A ) ) -> A e. Fin )
5 2 3 4 chnpolfz 
 |-  ( ( ( A e. Fin /\ .< Po A ) /\ x e. ( .< Chain A ) ) -> ( # ` x ) e. ( 0 ... ( # ` A ) ) )
6 risset 
 |-  ( ( # ` x ) e. ( 0 ... ( # ` A ) ) <-> E. n e. ( 0 ... ( # ` A ) ) n = ( # ` x ) )
7 eqcom 
 |-  ( n = ( # ` x ) <-> ( # ` x ) = n )
8 7 rexbii 
 |-  ( E. n e. ( 0 ... ( # ` A ) ) n = ( # ` x ) <-> E. n e. ( 0 ... ( # ` A ) ) ( # ` x ) = n )
9 6 8 bitri 
 |-  ( ( # ` x ) e. ( 0 ... ( # ` A ) ) <-> E. n e. ( 0 ... ( # ` A ) ) ( # ` x ) = n )
10 5 9 sylib 
 |-  ( ( ( A e. Fin /\ .< Po A ) /\ x e. ( .< Chain A ) ) -> E. n e. ( 0 ... ( # ` A ) ) ( # ` x ) = n )
11 10 rabeqcda 
 |-  ( ( A e. Fin /\ .< Po A ) -> { x e. ( .< Chain A ) | E. n e. ( 0 ... ( # ` A ) ) ( # ` x ) = n } = ( .< Chain A ) )
12 1 11 eqtr2id 
 |-  ( ( A e. Fin /\ .< Po A ) -> ( .< Chain A ) = U_ n e. ( 0 ... ( # ` A ) ) { x e. ( .< Chain A ) | ( # ` x ) = n } )
13 fzfid 
 |-  ( ( A e. Fin /\ .< Po A ) -> ( 0 ... ( # ` A ) ) e. Fin )
14 chnflenfi 
 |-  ( A e. Fin -> { x e. ( .< Chain A ) | ( # ` x ) = n } e. Fin )
15 14 adantr 
 |-  ( ( A e. Fin /\ .< Po A ) -> { x e. ( .< Chain A ) | ( # ` x ) = n } e. Fin )
16 15 ralrimivw 
 |-  ( ( A e. Fin /\ .< Po A ) -> A. n e. ( 0 ... ( # ` A ) ) { x e. ( .< Chain A ) | ( # ` x ) = n } e. Fin )
17 iunfi 
 |-  ( ( ( 0 ... ( # ` A ) ) e. Fin /\ A. n e. ( 0 ... ( # ` A ) ) { x e. ( .< Chain A ) | ( # ` x ) = n } e. Fin ) -> U_ n e. ( 0 ... ( # ` A ) ) { x e. ( .< Chain A ) | ( # ` x ) = n } e. Fin )
18 13 16 17 syl2anc 
 |-  ( ( A e. Fin /\ .< Po A ) -> U_ n e. ( 0 ... ( # ` A ) ) { x e. ( .< Chain A ) | ( # ` x ) = n } e. Fin )
19 12 18 eqeltrd 
 |-  ( ( A e. Fin /\ .< Po A ) -> ( .< Chain A ) e. Fin )