This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )