Metamath Proof Explorer

Theorem fin34i

Description: Inference from isfin3-4 . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin34i 
|- ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. x e. _om ( G ` x ) C_ ( G ` suc x ) ) -> U. ran G e. ran G )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( y e. ~P A |-> ( A \ y ) ) = ( y e. ~P A |-> ( A \ y ) )
2 1 isf34lem7 
 |-  ( ( A e. Fin3 /\ G : _om --> ~P A /\ A. x e. _om ( G ` x ) C_ ( G ` suc x ) ) -> U. ran G e. ran G )