Metamath Proof Explorer

Theorem fin23lem33

Description: Lemma for fin23 . Discharge hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypothesis fin23lem33.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 fin23lem33 
|- ( G e. F -> E. f A. b ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) )

Proof

Step Hyp Ref Expression
1 fin23lem33.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 fveq2 
 |-  ( j = c -> ( e ` j ) = ( e ` c ) )
3 2 ineq1d 
 |-  ( j = c -> ( ( e ` j ) i^i k ) = ( ( e ` c ) i^i k ) )
4 3 eqeq1d 
 |-  ( j = c -> ( ( ( e ` j ) i^i k ) = (/) <-> ( ( e ` c ) i^i k ) = (/) ) )
5 4 3 ifbieq2d 
 |-  ( j = c -> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) = if ( ( ( e ` c ) i^i k ) = (/) , k , ( ( e ` c ) i^i k ) ) )
6 ineq2 
 |-  ( k = d -> ( ( e ` c ) i^i k ) = ( ( e ` c ) i^i d ) )
7 6 eqeq1d 
 |-  ( k = d -> ( ( ( e ` c ) i^i k ) = (/) <-> ( ( e ` c ) i^i d ) = (/) ) )
8 id 
 |-  ( k = d -> k = d )
9 7 8 6 ifbieq12d 
 |-  ( k = d -> if ( ( ( e ` c ) i^i k ) = (/) , k , ( ( e ` c ) i^i k ) ) = if ( ( ( e ` c ) i^i d ) = (/) , d , ( ( e ` c ) i^i d ) ) )
10 5 9 cbvmpov 
 |-  ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) = ( c e. _om , d e. _V |-> if ( ( ( e ` c ) i^i d ) = (/) , d , ( ( e ` c ) i^i d ) ) )
11 eqid 
 |-  U. ran e = U. ran e
12 seqomeq12 
 |-  ( ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) = ( c e. _om , d e. _V |-> if ( ( ( e ` c ) i^i d ) = (/) , d , ( ( e ` c ) i^i d ) ) ) /\ U. ran e = U. ran e ) -> seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) = seqom ( ( c e. _om , d e. _V |-> if ( ( ( e ` c ) i^i d ) = (/) , d , ( ( e ` c ) i^i d ) ) ) , U. ran e ) )
13 10 11 12 mp2an 
 |-  seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) = seqom ( ( c e. _om , d e. _V |-> if ( ( ( e ` c ) i^i d ) = (/) , d , ( ( e ` c ) i^i d ) ) ) , U. ran e )
14 fveq2 
 |-  ( l = y -> ( e ` l ) = ( e ` y ) )
15 14 sseq2d 
 |-  ( l = y -> ( |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) <-> |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` y ) ) )
16 15 cbvrabv 
 |-  { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } = { y e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` y ) }
17 eqid 
 |-  ( g e. _om |-> ( iota_ x e. { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ( x i^i { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ~~ g ) ) = ( g e. _om |-> ( iota_ x e. { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ( x i^i { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ~~ g ) )
18 eqid 
 |-  ( g e. _om |-> ( iota_ x e. ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ( x i^i ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ) ~~ g ) ) = ( g e. _om |-> ( iota_ x e. ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ( x i^i ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ) ~~ g ) )
19 eqid 
 |-  if ( { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } e. Fin , ( e o. ( g e. _om |-> ( iota_ x e. ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ( x i^i ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ) ~~ g ) ) ) , ( ( i e. { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } |-> ( ( e ` i ) \ |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) ) ) o. ( g e. _om |-> ( iota_ x e. { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ( x i^i { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ~~ g ) ) ) ) = if ( { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } e. Fin , ( e o. ( g e. _om |-> ( iota_ x e. ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ( x i^i ( _om \ { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ) ~~ g ) ) ) , ( ( i e. { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } |-> ( ( e ` i ) \ |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) ) ) o. ( g e. _om |-> ( iota_ x e. { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ( x i^i { l e. _om | |^| ran seqom ( ( j e. _om , k e. _V |-> if ( ( ( e ` j ) i^i k ) = (/) , k , ( ( e ` j ) i^i k ) ) ) , U. ran e ) C_ ( e ` l ) } ) ~~ g ) ) ) )
20 13 1 16 17 18 19 fin23lem32 
 |-  ( G e. F -> E. f A. b ( ( b : _om -1-1-> _V /\ U. ran b C_ G ) -> ( ( f ` b ) : _om -1-1-> _V /\ U. ran ( f ` b ) C. U. ran b ) ) )