Metamath Proof Explorer

Theorem isf32lem11

Description: Lemma for isfin3-2 . Remove hypotheses from isf32lem10 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion 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 )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : _om --> ~P G /\ A. b e. _om ( F ` suc b ) C_ ( F ` b ) /\ -. |^| ran F e. ran F ) -> F : _om --> ~P G )
2 suceq 
 |-  ( b = c -> suc b = suc c )
3 2 fveq2d 
 |-  ( b = c -> ( F ` suc b ) = ( F ` suc c ) )
4 fveq2 
 |-  ( b = c -> ( F ` b ) = ( F ` c ) )
5 3 4 sseq12d 
 |-  ( b = c -> ( ( F ` suc b ) C_ ( F ` b ) <-> ( F ` suc c ) C_ ( F ` c ) ) )
6 5 cbvralvw 
 |-  ( A. b e. _om ( F ` suc b ) C_ ( F ` b ) <-> A. c e. _om ( F ` suc c ) C_ ( F ` c ) )
7 6 biimpi 
 |-  ( A. b e. _om ( F ` suc b ) C_ ( F ` b ) -> A. c e. _om ( F ` suc c ) C_ ( F ` c ) )
8 7 3ad2ant2 
 |-  ( ( F : _om --> ~P G /\ A. b e. _om ( F ` suc b ) C_ ( F ` b ) /\ -. |^| ran F e. ran F ) -> A. c e. _om ( F ` suc c ) C_ ( F ` c ) )
9 simp3 
 |-  ( ( F : _om --> ~P G /\ A. b e. _om ( F ` suc b ) C_ ( F ` b ) /\ -. |^| ran F e. ran F ) -> -. |^| ran F e. ran F )
10 suceq 
 |-  ( e = d -> suc e = suc d )
11 10 fveq2d 
 |-  ( e = d -> ( F ` suc e ) = ( F ` suc d ) )
12 fveq2 
 |-  ( e = d -> ( F ` e ) = ( F ` d ) )
13 11 12 psseq12d 
 |-  ( e = d -> ( ( F ` suc e ) C. ( F ` e ) <-> ( F ` suc d ) C. ( F ` d ) ) )
14 13 cbvrabv 
 |-  { e e. _om | ( F ` suc e ) C. ( F ` e ) } = { d e. _om | ( F ` suc d ) C. ( F ` d ) }
15 eqid 
 |-  ( f e. _om |-> ( iota_ g e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } ( g i^i { e e. _om | ( F ` suc e ) C. ( F ` e ) } ) ~~ f ) ) = ( f e. _om |-> ( iota_ g e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } ( g i^i { e e. _om | ( F ` suc e ) C. ( F ` e ) } ) ~~ f ) )
16 eqid 
 |-  ( ( h e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } |-> ( ( F ` h ) \ ( F ` suc h ) ) ) o. ( f e. _om |-> ( iota_ g e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } ( g i^i { e e. _om | ( F ` suc e ) C. ( F ` e ) } ) ~~ f ) ) ) = ( ( h e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } |-> ( ( F ` h ) \ ( F ` suc h ) ) ) o. ( f e. _om |-> ( iota_ g e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } ( g i^i { e e. _om | ( F ` suc e ) C. ( F ` e ) } ) ~~ f ) ) )
17 eqid 
 |-  ( k e. G |-> ( iota l ( l e. _om /\ k e. ( ( ( h e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } |-> ( ( F ` h ) \ ( F ` suc h ) ) ) o. ( f e. _om |-> ( iota_ g e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } ( g i^i { e e. _om | ( F ` suc e ) C. ( F ` e ) } ) ~~ f ) ) ) ` l ) ) ) ) = ( k e. G |-> ( iota l ( l e. _om /\ k e. ( ( ( h e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } |-> ( ( F ` h ) \ ( F ` suc h ) ) ) o. ( f e. _om |-> ( iota_ g e. { e e. _om | ( F ` suc e ) C. ( F ` e ) } ( g i^i { e e. _om | ( F ` suc e ) C. ( F ` e ) } ) ~~ f ) ) ) ` l ) ) ) )
18 1 8 9 14 15 16 17 isf32lem10 
 |-  ( ( F : _om --> ~P G /\ A. b e. _om ( F ` suc b ) C_ ( F ` b ) /\ -. |^| ran F e. ran F ) -> ( G e. V -> _om ~<_* G ) )
19 18 impcom 
 |-  ( ( G e. V /\ ( F : _om --> ~P G /\ A. b e. _om ( F ` suc b ) C_ ( F ` b ) /\ -. |^| ran F e. ran F ) ) -> _om ~<_* G )