Step |
Hyp |
Ref |
Expression |
1 |
|
isfin3ds.f |
|- F = { g | A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) } |
2 |
|
suceq |
|- ( b = x -> suc b = suc x ) |
3 |
2
|
fveq2d |
|- ( b = x -> ( a ` suc b ) = ( a ` suc x ) ) |
4 |
|
fveq2 |
|- ( b = x -> ( a ` b ) = ( a ` x ) ) |
5 |
3 4
|
sseq12d |
|- ( b = x -> ( ( a ` suc b ) C_ ( a ` b ) <-> ( a ` suc x ) C_ ( a ` x ) ) ) |
6 |
5
|
cbvralvw |
|- ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) <-> A. x e. _om ( a ` suc x ) C_ ( a ` x ) ) |
7 |
|
fveq1 |
|- ( a = f -> ( a ` suc x ) = ( f ` suc x ) ) |
8 |
|
fveq1 |
|- ( a = f -> ( a ` x ) = ( f ` x ) ) |
9 |
7 8
|
sseq12d |
|- ( a = f -> ( ( a ` suc x ) C_ ( a ` x ) <-> ( f ` suc x ) C_ ( f ` x ) ) ) |
10 |
9
|
ralbidv |
|- ( a = f -> ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) <-> A. x e. _om ( f ` suc x ) C_ ( f ` x ) ) ) |
11 |
6 10
|
syl5bb |
|- ( a = f -> ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) <-> A. x e. _om ( f ` suc x ) C_ ( f ` x ) ) ) |
12 |
|
rneq |
|- ( a = f -> ran a = ran f ) |
13 |
12
|
inteqd |
|- ( a = f -> |^| ran a = |^| ran f ) |
14 |
13 12
|
eleq12d |
|- ( a = f -> ( |^| ran a e. ran a <-> |^| ran f e. ran f ) ) |
15 |
11 14
|
imbi12d |
|- ( a = f -> ( ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) <-> ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) ) |
16 |
15
|
cbvralvw |
|- ( A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) <-> A. f e. ( ~P g ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) |
17 |
|
pweq |
|- ( g = A -> ~P g = ~P A ) |
18 |
17
|
oveq1d |
|- ( g = A -> ( ~P g ^m _om ) = ( ~P A ^m _om ) ) |
19 |
18
|
raleqdv |
|- ( g = A -> ( A. f e. ( ~P g ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) ) |
20 |
16 19
|
syl5bb |
|- ( g = A -> ( A. a e. ( ~P g ^m _om ) ( A. b e. _om ( a ` suc b ) C_ ( a ` b ) -> |^| ran a e. ran a ) <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) ) |
21 |
20 1
|
elab2g |
|- ( A e. V -> ( A e. F <-> A. f e. ( ~P A ^m _om ) ( A. x e. _om ( f ` suc x ) C_ ( f ` x ) -> |^| ran f e. ran f ) ) ) |