Theorem tfsnfin

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	tfsnfin	⊢ ( ( 𝐴 Fn 𝐵 ∧ 𝐵 ∈ On ) → ( ¬ 𝐴 ∈ Fin ↔ ω ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐴 Fn 𝐵 → Fun 𝐴 )
2		fundmfibi	⊢ ( Fun 𝐴 → ( 𝐴 ∈ Fin ↔ dom 𝐴 ∈ Fin ) )
3	1 2	syl	⊢ ( 𝐴 Fn 𝐵 → ( 𝐴 ∈ Fin ↔ dom 𝐴 ∈ Fin ) )
4		fndm	⊢ ( 𝐴 Fn 𝐵 → dom 𝐴 = 𝐵 )
5	4	eleq1d	⊢ ( 𝐴 Fn 𝐵 → ( dom 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
6	3 5	bitrd	⊢ ( 𝐴 Fn 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
7		onfin	⊢ ( 𝐵 ∈ On → ( 𝐵 ∈ Fin ↔ 𝐵 ∈ ω ) )
8	6 7	sylan9bb	⊢ ( ( 𝐴 Fn 𝐵 ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ ω ) )
9	8	notbid	⊢ ( ( 𝐴 Fn 𝐵 ∧ 𝐵 ∈ On ) → ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐵 ∈ ω ) )
10		omelon	⊢ ω ∈ On
11		simpr	⊢ ( ( 𝐴 Fn 𝐵 ∧ 𝐵 ∈ On ) → 𝐵 ∈ On )
12		ontri1	⊢ ( ( ω ∈ On ∧ 𝐵 ∈ On ) → ( ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω ) )
13	10 11 12	sylancr	⊢ ( ( 𝐴 Fn 𝐵 ∧ 𝐵 ∈ On ) → ( ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω ) )
14	9 13	bitr4d	⊢ ( ( 𝐴 Fn 𝐵 ∧ 𝐵 ∈ On ) → ( ¬ 𝐴 ∈ Fin ↔ ω ⊆ 𝐵 ) )