This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ordfin 
 |-  ( Ord B -> ( B e. Fin <-> B e. _om ) )
8 6 7 sylan9bb 
 |-  ( ( A Fn B /\ Ord B ) -> ( A e. Fin <-> B e. _om ) )
9 8 notbid 
 |-  ( ( A Fn B /\ Ord B ) -> ( -. A e. Fin <-> -. B e. _om ) )
10 ordom 
 |-  Ord _om
11 ordtri1 
 |-  ( ( Ord _om /\ Ord B ) -> ( _om C_ B <-> -. B e. _om ) )
12 10 11 mpan 
 |-  ( Ord B -> ( _om C_ B <-> -. B e. _om ) )
13 12 adantl 
 |-  ( ( A Fn B /\ Ord B ) -> ( _om C_ B <-> -. B e. _om ) )
14 9 13 bitr4d 
 |-  ( ( A Fn B /\ Ord B ) -> ( -. A e. Fin <-> _om C_ B ) )