Step |
Hyp |
Ref |
Expression |
1 |
|
tposfun |
|- ( Fun F -> Fun tpos F ) |
2 |
1
|
a1i |
|- ( Rel A -> ( Fun F -> Fun tpos F ) ) |
3 |
|
dmtpos |
|- ( Rel dom F -> dom tpos F = `' dom F ) |
4 |
3
|
a1i |
|- ( dom F = A -> ( Rel dom F -> dom tpos F = `' dom F ) ) |
5 |
|
releq |
|- ( dom F = A -> ( Rel dom F <-> Rel A ) ) |
6 |
|
cnveq |
|- ( dom F = A -> `' dom F = `' A ) |
7 |
6
|
eqeq2d |
|- ( dom F = A -> ( dom tpos F = `' dom F <-> dom tpos F = `' A ) ) |
8 |
4 5 7
|
3imtr3d |
|- ( dom F = A -> ( Rel A -> dom tpos F = `' A ) ) |
9 |
8
|
com12 |
|- ( Rel A -> ( dom F = A -> dom tpos F = `' A ) ) |
10 |
2 9
|
anim12d |
|- ( Rel A -> ( ( Fun F /\ dom F = A ) -> ( Fun tpos F /\ dom tpos F = `' A ) ) ) |
11 |
|
df-fn |
|- ( F Fn A <-> ( Fun F /\ dom F = A ) ) |
12 |
|
df-fn |
|- ( tpos F Fn `' A <-> ( Fun tpos F /\ dom tpos F = `' A ) ) |
13 |
10 11 12
|
3imtr4g |
|- ( Rel A -> ( F Fn A -> tpos F Fn `' A ) ) |