Metamath Proof Explorer

Theorem tfsnfin2

Description: A transfinite sequence is infinite iff its domain is greater than or equal to omega. Theorem 5 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 1-Mar-2025)

Ref Expression
Assertion tfsnfin2 ⊢ A Fn B ∧ Ord ⁡ B → ¬ A ∈ Fin ↔ ω ⊆ B

Proof

Step Hyp Ref Expression
1 fnfun ⊢ A Fn B → Fun ⁡ A
2 fundmfibi ⊢ Fun ⁡ A → A ∈ Fin ↔ dom ⁡ A ∈ Fin
3 1 2 syl ⊢ A Fn B → A ∈ Fin ↔ dom ⁡ A ∈ Fin
4 fndm ⊢ A Fn B → dom ⁡ A = B
5 4 eleq1d ⊢ A Fn B → dom ⁡ A ∈ Fin ↔ B ∈ Fin
6 3 5 bitrd ⊢ A Fn B → A ∈ Fin ↔ B ∈ Fin
7 ordfin ⊢ Ord ⁡ B → B ∈ Fin ↔ B ∈ ω
8 6 7 sylan9bb ⊢ A Fn B ∧ Ord ⁡ B → A ∈ Fin ↔ B ∈ ω
9 8 notbid ⊢ A Fn B ∧ Ord ⁡ B → ¬ A ∈ Fin ↔ ¬ B ∈ ω
10 ordom ⊢ Ord ⁡ ω
11 ordtri1 ⊢ Ord ⁡ ω ∧ Ord ⁡ B → ω ⊆ B ↔ ¬ B ∈ ω
12 10 11 mpan ⊢ Ord ⁡ B → ω ⊆ B ↔ ¬ B ∈ ω
13 12 adantl ⊢ A Fn B ∧ Ord ⁡ B → ω ⊆ B ↔ ¬ B ∈ ω
14 9 13 bitr4d ⊢ A Fn B ∧ Ord ⁡ B → ¬ A ∈ Fin ↔ ω ⊆ B