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
|
syl5bb |
|- ( 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 ) } |