Step |
Hyp |
Ref |
Expression |
1 |
|
offvalfv.a |
|- ( ph -> A e. V ) |
2 |
|
offvalfv.f |
|- ( ph -> F Fn A ) |
3 |
|
offvalfv.g |
|- ( ph -> G Fn A ) |
4 |
|
fnfvelrn |
|- ( ( F Fn A /\ x e. A ) -> ( F ` x ) e. ran F ) |
5 |
2 4
|
sylan |
|- ( ( ph /\ x e. A ) -> ( F ` x ) e. ran F ) |
6 |
|
fnfvelrn |
|- ( ( G Fn A /\ x e. A ) -> ( G ` x ) e. ran G ) |
7 |
3 6
|
sylan |
|- ( ( ph /\ x e. A ) -> ( G ` x ) e. ran G ) |
8 |
|
dffn5 |
|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) ) |
9 |
2 8
|
sylib |
|- ( ph -> F = ( x e. A |-> ( F ` x ) ) ) |
10 |
|
dffn5 |
|- ( G Fn A <-> G = ( x e. A |-> ( G ` x ) ) ) |
11 |
3 10
|
sylib |
|- ( ph -> G = ( x e. A |-> ( G ` x ) ) ) |
12 |
1 5 7 9 11
|
offval2 |
|- ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) ) |