Theorem isfin3-2

Description: Weakly Dedekind-infinite sets are exactly those which can be mapped onto _om . (Contributed by Stefan O'Rear, 6-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin3-2	|- ( A e. V -> ( A e. Fin3 <-> -. _om ~<_* A ) )

Proof

Step	Hyp	Ref	Expression
1		isfin32i	|- ( A e. Fin3 -> -. _om ~<_* A )
2		isf33lem	|- Fin3 = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
3	2	isf32lem12	|- ( A e. V -> ( -. _om ~<_* A -> A e. Fin3 ) )
4	1 3	impbid2	|- ( A e. V -> ( A e. Fin3 <-> -. _om ~<_* A ) )