Theorem fin33i

Description: Inference from isfin3-3 . (This is actually a bit stronger than isfin3-3 because it does not assume F is a set and does not use the Axiom of Infinity either.) (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	fin33i	|- ( ( A e. Fin3 /\ F : _om --> ~P A /\ A. x e. _om ( F ` suc x ) C_ ( F ` x ) ) -> |^| ran F e. ran F )

Proof

Step	Hyp	Ref	Expression
1		isfin32i	|- ( A e. Fin3 -> -. _om ~<_* A )
2	1	3ad2ant1	|- ( ( A e. Fin3 /\ F : _om --> ~P A /\ A. x e. _om ( F ` suc x ) C_ ( F ` x ) ) -> -. _om ~<_* A )
3		isf32lem11	|- ( ( A e. Fin3 /\ ( F : _om --> ~P A /\ A. x e. _om ( F ` suc x ) C_ ( F ` x ) /\ -. |^| ran F e. ran F ) ) -> _om ~<_* A )
4	3	3exp2	|- ( A e. Fin3 -> ( F : _om --> ~P A -> ( A. x e. _om ( F ` suc x ) C_ ( F ` x ) -> ( -. |^| ran F e. ran F -> _om ~<_* A ) ) ) )
5	4	3imp	|- ( ( A e. Fin3 /\ F : _om --> ~P A /\ A. x e. _om ( F ` suc x ) C_ ( F ` x ) ) -> ( -. |^| ran F e. ran F -> _om ~<_* A ) )
6	2 5	mt3d	|- ( ( A e. Fin3 /\ F : _om --> ~P A /\ A. x e. _om ( F ` suc x ) C_ ( F ` x ) ) -> |^| ran F e. ran F )