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 ) )