This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )