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 ∈ Fin ∧ < ˙ Po A → Chain A < ˙ ∈ Fin

Proof

Step Hyp Ref Expression
1 iunrab ⊢ ⋃ n = 0 A x ∈ Chain A < ˙ | x = n = x ∈ Chain A < ˙ | ∃ n ∈ 0 … A x = n
2 simplr ⊢ A ∈ Fin ∧ < ˙ Po A ∧ x ∈ Chain A < ˙ → < ˙ Po A
3 simpr ⊢ A ∈ Fin ∧ < ˙ Po A ∧ x ∈ Chain A < ˙ → x ∈ Chain A < ˙
4 simpll ⊢ A ∈ Fin ∧ < ˙ Po A ∧ x ∈ Chain A < ˙ → A ∈ Fin
5 2 3 4 chnpolfz ⊢ A ∈ Fin ∧ < ˙ Po A ∧ x ∈ Chain A < ˙ → x ∈ 0 … A
6 risset ⊢ x ∈ 0 … A ↔ ∃ n ∈ 0 … A n = x
7 eqcom ⊢ n = x ↔ x = n
8 7 rexbii ⊢ ∃ n ∈ 0 … A n = x ↔ ∃ n ∈ 0 … A x = n
9 6 8 bitri ⊢ x ∈ 0 … A ↔ ∃ n ∈ 0 … A x = n
10 5 9 sylib ⊢ A ∈ Fin ∧ < ˙ Po A ∧ x ∈ Chain A < ˙ → ∃ n ∈ 0 … A x = n
11 10 rabeqcda ⊢ A ∈ Fin ∧ < ˙ Po A → x ∈ Chain A < ˙ | ∃ n ∈ 0 … A x = n = Chain A < ˙
12 1 11 eqtr2id ⊢ A ∈ Fin ∧ < ˙ Po A → Chain A < ˙ = ⋃ n = 0 A x ∈ Chain A < ˙ | x = n
13 fzfid ⊢ A ∈ Fin ∧ < ˙ Po A → 0 … A ∈ Fin
14 chnflenfi ⊢ A ∈ Fin → x ∈ Chain A < ˙ | x = n ∈ Fin
15 14 adantr ⊢ A ∈ Fin ∧ < ˙ Po A → x ∈ Chain A < ˙ | x = n ∈ Fin
16 15 ralrimivw ⊢ A ∈ Fin ∧ < ˙ Po A → ∀ n ∈ 0 … A x ∈ Chain A < ˙ | x = n ∈ Fin
17 iunfi ⊢ 0 … A ∈ Fin ∧ ∀ n ∈ 0 … A x ∈ Chain A < ˙ | x = n ∈ Fin → ⋃ n = 0 A x ∈ Chain A < ˙ | x = n ∈ Fin
18 13 16 17 syl2anc ⊢ A ∈ Fin ∧ < ˙ Po A → ⋃ n = 0 A x ∈ Chain A < ˙ | x = n ∈ Fin
19 12 18 eqeltrd ⊢ A ∈ Fin ∧ < ˙ Po A → Chain A < ˙ ∈ Fin