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	|- ( ( A Fn B /\ B e. On ) -> ( -. A e. Fin <-> _om C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( A Fn B -> Fun A )
2		fundmfibi	|- ( Fun A -> ( A e. Fin <-> dom A e. Fin ) )
3	1 2	syl	|- ( A Fn B -> ( A e. Fin <-> dom A e. Fin ) )
4		fndm	|- ( A Fn B -> dom A = B )
5	4	eleq1d	|- ( A Fn B -> ( dom A e. Fin <-> B e. Fin ) )
6	3 5	bitrd	|- ( A Fn B -> ( A e. Fin <-> B e. Fin ) )
7		onfin	|- ( B e. On -> ( B e. Fin <-> B e. _om ) )
8	6 7	sylan9bb	|- ( ( A Fn B /\ B e. On ) -> ( A e. Fin <-> B e. _om ) )
9	8	notbid	|- ( ( A Fn B /\ B e. On ) -> ( -. A e. Fin <-> -. B e. _om ) )
10		omelon	|- _om e. On
11		simpr	|- ( ( A Fn B /\ B e. On ) -> B e. On )
12		ontri1	|- ( ( _om e. On /\ B e. On ) -> ( _om C_ B <-> -. B e. _om ) )
13	10 11 12	sylancr	|- ( ( A Fn B /\ B e. On ) -> ( _om C_ B <-> -. B e. _om ) )
14	9 13	bitr4d	|- ( ( A Fn B /\ B e. On ) -> ( -. A e. Fin <-> _om C_ B ) )