Metamath Proof Explorer


Theorem ofrn2

Description: The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-2017)

Ref Expression
Hypotheses ofrn.1
|- ( ph -> F : A --> B )
ofrn.2
|- ( ph -> G : A --> B )
ofrn.3
|- ( ph -> .+ : ( B X. B ) --> C )
ofrn.4
|- ( ph -> A e. V )
Assertion ofrn2
|- ( ph -> ran ( F oF .+ G ) C_ ( .+ " ( ran F X. ran G ) ) )

Proof

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 ) ) )