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 )