Metamath Proof Explorer


Theorem 1stcof

Description: Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007)

Ref Expression
Assertion 1stcof
|- ( F : A --> ( B X. C ) -> ( 1st o. F ) : A --> B )

Proof

Step Hyp Ref Expression
1 fo1st
 |-  1st : _V -onto-> _V
2 fofn
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
3 1 2 ax-mp
 |-  1st 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
 |-  ( ( 1st Fn _V /\ F : A --> _V ) -> ( 1st o. F ) Fn A )
8 3 6 7 sylancr
 |-  ( F : A --> ( B X. C ) -> ( 1st o. F ) Fn A )
9 rnco
 |-  ran ( 1st o. F ) = ran ( 1st |` ran F )
10 frn
 |-  ( F : A --> ( B X. C ) -> ran F C_ ( B X. C ) )
11 ssres2
 |-  ( ran F C_ ( B X. C ) -> ( 1st |` ran F ) C_ ( 1st |` ( B X. C ) ) )
12 rnss
 |-  ( ( 1st |` ran F ) C_ ( 1st |` ( B X. C ) ) -> ran ( 1st |` ran F ) C_ ran ( 1st |` ( B X. C ) ) )
13 10 11 12 3syl
 |-  ( F : A --> ( B X. C ) -> ran ( 1st |` ran F ) C_ ran ( 1st |` ( B X. C ) ) )
14 f1stres
 |-  ( 1st |` ( B X. C ) ) : ( B X. C ) --> B
15 frn
 |-  ( ( 1st |` ( B X. C ) ) : ( B X. C ) --> B -> ran ( 1st |` ( B X. C ) ) C_ B )
16 14 15 ax-mp
 |-  ran ( 1st |` ( B X. C ) ) C_ B
17 13 16 sstrdi
 |-  ( F : A --> ( B X. C ) -> ran ( 1st |` ran F ) C_ B )
18 9 17 eqsstrid
 |-  ( F : A --> ( B X. C ) -> ran ( 1st o. F ) C_ B )
19 df-f
 |-  ( ( 1st o. F ) : A --> B <-> ( ( 1st o. F ) Fn A /\ ran ( 1st o. F ) C_ B ) )
20 8 18 19 sylanbrc
 |-  ( F : A --> ( B X. C ) -> ( 1st o. F ) : A --> B )