Metamath Proof Explorer


Theorem isfin4-2

Description: Alternate definition of IV-finite sets: they lack a denumerable subset. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion isfin4-2
|- ( A e. V -> ( A e. Fin4 <-> -. _om ~<_ A ) )

Proof

Step Hyp Ref Expression
1 isfin4
 |-  ( A e. V -> ( A e. Fin4 <-> -. E. x ( x C. A /\ x ~~ A ) ) )
2 infpssr
 |-  ( ( x C. A /\ x ~~ A ) -> _om ~<_ A )
3 2 exlimiv
 |-  ( E. x ( x C. A /\ x ~~ A ) -> _om ~<_ A )
4 infpss
 |-  ( _om ~<_ A -> E. x ( x C. A /\ x ~~ A ) )
5 3 4 impbii
 |-  ( E. x ( x C. A /\ x ~~ A ) <-> _om ~<_ A )
6 5 notbii
 |-  ( -. E. x ( x C. A /\ x ~~ A ) <-> -. _om ~<_ A )
7 1 6 bitrdi
 |-  ( A e. V -> ( A e. Fin4 <-> -. _om ~<_ A ) )