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