Step |
Hyp |
Ref |
Expression |
1 |
|
ofrn.1 |
|- ( ph -> F : A --> B ) |
2 |
|
ofrn.2 |
|- ( ph -> G : A --> B ) |
3 |
|
ofrn.3 |
|- ( ph -> .+ : ( B X. B ) --> C ) |
4 |
|
ofrn.4 |
|- ( ph -> A e. V ) |
5 |
1
|
ffnd |
|- ( ph -> F Fn A ) |
6 |
|
simprl |
|- ( ( ph /\ ( a e. A /\ z = ( ( F ` a ) .+ ( G ` a ) ) ) ) -> a e. A ) |
7 |
|
fnfvelrn |
|- ( ( F Fn A /\ a e. A ) -> ( F ` a ) e. ran F ) |
8 |
5 6 7
|
syl2an2r |
|- ( ( ph /\ ( a e. A /\ z = ( ( F ` a ) .+ ( G ` a ) ) ) ) -> ( F ` a ) e. ran F ) |
9 |
2
|
ffnd |
|- ( ph -> G Fn A ) |
10 |
|
fnfvelrn |
|- ( ( G Fn A /\ a e. A ) -> ( G ` a ) e. ran G ) |
11 |
9 6 10
|
syl2an2r |
|- ( ( ph /\ ( a e. A /\ z = ( ( F ` a ) .+ ( G ` a ) ) ) ) -> ( G ` a ) e. ran G ) |
12 |
|
simprr |
|- ( ( ph /\ ( a e. A /\ z = ( ( F ` a ) .+ ( G ` a ) ) ) ) -> z = ( ( F ` a ) .+ ( G ` a ) ) ) |
13 |
|
rspceov |
|- ( ( ( F ` a ) e. ran F /\ ( G ` a ) e. ran G /\ z = ( ( F ` a ) .+ ( G ` a ) ) ) -> E. x e. ran F E. y e. ran G z = ( x .+ y ) ) |
14 |
8 11 12 13
|
syl3anc |
|- ( ( ph /\ ( a e. A /\ z = ( ( F ` a ) .+ ( G ` a ) ) ) ) -> E. x e. ran F E. y e. ran G z = ( x .+ y ) ) |
15 |
14
|
rexlimdvaa |
|- ( ph -> ( E. a e. A z = ( ( F ` a ) .+ ( G ` a ) ) -> E. x e. ran F E. y e. ran G z = ( x .+ y ) ) ) |
16 |
15
|
ss2abdv |
|- ( ph -> { z | E. a e. A z = ( ( F ` a ) .+ ( G ` a ) ) } C_ { z | E. x e. ran F E. y e. ran G z = ( x .+ y ) } ) |
17 |
|
inidm |
|- ( A i^i A ) = A |
18 |
|
eqidd |
|- ( ( ph /\ a e. A ) -> ( F ` a ) = ( F ` a ) ) |
19 |
|
eqidd |
|- ( ( ph /\ a e. A ) -> ( G ` a ) = ( G ` a ) ) |
20 |
5 9 4 4 17 18 19
|
offval |
|- ( ph -> ( F oF .+ G ) = ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) ) |
21 |
20
|
rneqd |
|- ( ph -> ran ( F oF .+ G ) = ran ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) ) |
22 |
|
eqid |
|- ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) = ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) |
23 |
22
|
rnmpt |
|- ran ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) = { z | E. a e. A z = ( ( F ` a ) .+ ( G ` a ) ) } |
24 |
21 23
|
eqtrdi |
|- ( ph -> ran ( F oF .+ G ) = { z | E. a e. A z = ( ( F ` a ) .+ ( G ` a ) ) } ) |
25 |
3
|
ffnd |
|- ( ph -> .+ Fn ( B X. B ) ) |
26 |
1
|
frnd |
|- ( ph -> ran F C_ B ) |
27 |
2
|
frnd |
|- ( ph -> ran G C_ B ) |
28 |
|
xpss12 |
|- ( ( ran F C_ B /\ ran G C_ B ) -> ( ran F X. ran G ) C_ ( B X. B ) ) |
29 |
26 27 28
|
syl2anc |
|- ( ph -> ( ran F X. ran G ) C_ ( B X. B ) ) |
30 |
|
ovelimab |
|- ( ( .+ Fn ( B X. B ) /\ ( ran F X. ran G ) C_ ( B X. B ) ) -> ( z e. ( .+ " ( ran F X. ran G ) ) <-> E. x e. ran F E. y e. ran G z = ( x .+ y ) ) ) |
31 |
25 29 30
|
syl2anc |
|- ( ph -> ( z e. ( .+ " ( ran F X. ran G ) ) <-> E. x e. ran F E. y e. ran G z = ( x .+ y ) ) ) |
32 |
31
|
abbi2dv |
|- ( ph -> ( .+ " ( ran F X. ran G ) ) = { z | E. x e. ran F E. y e. ran G z = ( x .+ y ) } ) |
33 |
16 24 32
|
3sstr4d |
|- ( ph -> ran ( F oF .+ G ) C_ ( .+ " ( ran F X. ran G ) ) ) |