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 )