Metamath Proof Explorer

Theorem infinf

Description: Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017)

Ref Expression
Assertion infinf 
|- ( A e. B -> ( -. A e. Fin <-> _om ~<_ A ) )

Proof

Step Hyp Ref Expression
1 isfinite 
 |-  ( A e. Fin <-> A ~< _om )
2 1 notbii 
 |-  ( -. A e. Fin <-> -. A ~< _om )
3 omex 
 |-  _om e. _V
4 domtri 
 |-  ( ( _om e. _V /\ A e. B ) -> ( _om ~<_ A <-> -. A ~< _om ) )
5 3 4 mpan 
 |-  ( A e. B -> ( _om ~<_ A <-> -. A ~< _om ) )
6 2 5 bitr4id 
 |-  ( A e. B -> ( -. A e. Fin <-> _om ~<_ A ) )