Metamath Proof Explorer

Theorem isf33lem

Description: Lemma for isfin3-3 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion isf33lem 
|- Fin3 = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }

Proof

Step Hyp Ref Expression
1 isfin32i 
 |-  ( f e. Fin3 -> -. _om ~<_* f )
2 fveq1 
 |-  ( a = b -> ( a ` suc x ) = ( b ` suc x ) )
3 fveq1 
 |-  ( a = b -> ( a ` x ) = ( b ` x ) )
4 2 3 sseq12d 
 |-  ( a = b -> ( ( a ` suc x ) C_ ( a ` x ) <-> ( b ` suc x ) C_ ( b ` x ) ) )
5 4 ralbidv 
 |-  ( a = b -> ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) <-> A. x e. _om ( b ` suc x ) C_ ( b ` x ) ) )
6 rneq 
 |-  ( a = b -> ran a = ran b )
7 6 inteqd 
 |-  ( a = b -> |^| ran a = |^| ran b )
8 7 6 eleq12d 
 |-  ( a = b -> ( |^| ran a e. ran a <-> |^| ran b e. ran b ) )
9 5 8 imbi12d 
 |-  ( a = b -> ( ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) <-> ( A. x e. _om ( b ` suc x ) C_ ( b ` x ) -> |^| ran b e. ran b ) ) )
10 9 cbvralvw 
 |-  ( A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) <-> A. b e. ( ~P g ^m _om ) ( A. x e. _om ( b ` suc x ) C_ ( b ` x ) -> |^| ran b e. ran b ) )
11 pweq 
 |-  ( g = y -> ~P g = ~P y )
12 11 oveq1d 
 |-  ( g = y -> ( ~P g ^m _om ) = ( ~P y ^m _om ) )
13 12 raleqdv 
 |-  ( g = y -> ( A. b e. ( ~P g ^m _om ) ( A. x e. _om ( b ` suc x ) C_ ( b ` x ) -> |^| ran b e. ran b ) <-> A. b e. ( ~P y ^m _om ) ( A. x e. _om ( b ` suc x ) C_ ( b ` x ) -> |^| ran b e. ran b ) ) )
14 10 13 bitrid 
 |-  ( g = y -> ( A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) <-> A. b e. ( ~P y ^m _om ) ( A. x e. _om ( b ` suc x ) C_ ( b ` x ) -> |^| ran b e. ran b ) ) )
15 14 cbvabv 
 |-  { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) } = { y | A. b e. ( ~P y ^m _om ) ( A. x e. _om ( b ` suc x ) C_ ( b ` x ) -> |^| ran b e. ran b ) }
16 15 isf32lem12 
 |-  ( f e. Fin3 -> ( -. _om ~<_* f -> f e. { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) } ) )
17 1 16 mpd 
 |-  ( f e. Fin3 -> f e. { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) } )
18 10 abbii 
 |-  { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) } = { g | A. b e. ( ~P g ^m _om ) ( A. x e. _om ( b ` suc x ) C_ ( b ` x ) -> |^| ran b e. ran b ) }
19 18 fin23lem41 
 |-  ( f e. { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) } -> f e. Fin3 )
20 17 19 impbii 
 |-  ( f e. Fin3 <-> f e. { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) } )
21 20 eqriv 
 |-  Fin3 = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }