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 ) |
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 ) |