Theorem isf32lem12

Description: Lemma for isfin3-2 . (Contributed by Stefan O'Rear, 6-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypothesis	isf32lem40.f	|- F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
Assertion	isf32lem12	|- ( G e. V -> ( -. _om ~<_* G -> G e. F ) )

Proof

Step	Hyp	Ref	Expression
1		isf32lem40.f	|- F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
2		elmapi	|- ( f e. ( ~P G ^m _om ) -> f : _om --> ~P G )
3		isf32lem11	|- ( ( G e. V /\ ( f : _om --> ~P G /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) /\ -. |^| ran f e. ran f ) ) -> _om ~<_* G )
4	3	expcom	|- ( ( f : _om --> ~P G /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) /\ -. |^| ran f e. ran f ) -> ( G e. V -> _om ~<_* G ) )
5	4	3expa	|- ( ( ( f : _om --> ~P G /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) /\ -. |^| ran f e. ran f ) -> ( G e. V -> _om ~<_* G ) )
6	5	impancom	|- ( ( ( f : _om --> ~P G /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) /\ G e. V ) -> ( -. |^| ran f e. ran f -> _om ~<_* G ) )
7	6	con1d	|- ( ( ( f : _om --> ~P G /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) /\ G e. V ) -> ( -. _om ~<_* G -> |^| ran f e. ran f ) )
8	7	exp31	|- ( f : _om --> ~P G -> ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> ( G e. V -> ( -. _om ~<_* G -> |^| ran f e. ran f ) ) ) )
9	2 8	syl	|- ( f e. ( ~P G ^m _om ) -> ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> ( G e. V -> ( -. _om ~<_* G -> |^| ran f e. ran f ) ) ) )
10	9	com4t	|- ( G e. V -> ( -. _om ~<_* G -> ( f e. ( ~P G ^m _om ) -> ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> |^| ran f e. ran f ) ) ) )
11	10	ralrimdv	|- ( G e. V -> ( -. _om ~<_* G -> A. f e. ( ~P G ^m _om ) ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> |^| ran f e. ran f ) ) )
12	1	isfin3ds	|- ( G e. V -> ( G e. F <-> A. f e. ( ~P G ^m _om ) ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> |^| ran f e. ran f ) ) )
13	11 12	sylibrd	|- ( G e. V -> ( -. _om ~<_* G -> G e. F ) )