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