Metamath Proof Explorer

Theorem 2ndcof

Description: Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012)

Ref Expression
Assertion 2ndcof 
|- ( F : A --> ( B X. C ) -> ( 2nd o. F ) : A --> C )

Proof

Step Hyp Ref Expression
1 fo2nd 
 |-  2nd : _V -onto-> _V
2 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
3 1 2 ax-mp 
 |-  2nd Fn _V
4 ffn 
 |-  ( F : A --> ( B X. C ) -> F Fn A )
5 dffn2 
 |-  ( F Fn A <-> F : A --> _V )
6 4 5 sylib 
 |-  ( F : A --> ( B X. C ) -> F : A --> _V )
7 fnfco 
 |-  ( ( 2nd Fn _V /\ F : A --> _V ) -> ( 2nd o. F ) Fn A )
8 3 6 7 sylancr 
 |-  ( F : A --> ( B X. C ) -> ( 2nd o. F ) Fn A )
9 rnco 
 |-  ran ( 2nd o. F ) = ran ( 2nd |` ran F )
10 frn 
 |-  ( F : A --> ( B X. C ) -> ran F C_ ( B X. C ) )
11 ssres2 
 |-  ( ran F C_ ( B X. C ) -> ( 2nd |` ran F ) C_ ( 2nd |` ( B X. C ) ) )
12 rnss 
 |-  ( ( 2nd |` ran F ) C_ ( 2nd |` ( B X. C ) ) -> ran ( 2nd |` ran F ) C_ ran ( 2nd |` ( B X. C ) ) )
13 10 11 12 3syl 
 |-  ( F : A --> ( B X. C ) -> ran ( 2nd |` ran F ) C_ ran ( 2nd |` ( B X. C ) ) )
14 f2ndres 
 |-  ( 2nd |` ( B X. C ) ) : ( B X. C ) --> C
15 frn 
 |-  ( ( 2nd |` ( B X. C ) ) : ( B X. C ) --> C -> ran ( 2nd |` ( B X. C ) ) C_ C )
16 14 15 ax-mp 
 |-  ran ( 2nd |` ( B X. C ) ) C_ C
17 13 16 sstrdi 
 |-  ( F : A --> ( B X. C ) -> ran ( 2nd |` ran F ) C_ C )
18 9 17 eqsstrid 
 |-  ( F : A --> ( B X. C ) -> ran ( 2nd o. F ) C_ C )
19 df-f 
 |-  ( ( 2nd o. F ) : A --> C <-> ( ( 2nd o. F ) Fn A /\ ran ( 2nd o. F ) C_ C ) )
20 8 18 19 sylanbrc 
 |-  ( F : A --> ( B X. C ) -> ( 2nd o. F ) : A --> C )