1stcof

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

		Ref	Expression
	Assertion	1stcof	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 1^st ∘ 𝐹 ) : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fo1st	⊢ 1^st : V –onto→ V
2		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
3	1 2	ax-mp	⊢ 1^st Fn V
4		ffn	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → 𝐹 Fn 𝐴 )
5		dffn2	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ V )
6	4 5	sylib	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → 𝐹 : 𝐴 ⟶ V )
7		fnfco	⊢ ( ( 1^st Fn V ∧ 𝐹 : 𝐴 ⟶ V ) → ( 1^st ∘ 𝐹 ) Fn 𝐴 )
8	3 6 7	sylancr	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 1^st ∘ 𝐹 ) Fn 𝐴 )
9		rnco	⊢ ran ( 1^st ∘ 𝐹 ) = ran ( 1^st ↾ ran 𝐹 )
10		frn	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran 𝐹 ⊆ ( 𝐵 × 𝐶 ) )
11		ssres2	⊢ ( ran 𝐹 ⊆ ( 𝐵 × 𝐶 ) → ( 1^st ↾ ran 𝐹 ) ⊆ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) )
12		rnss	⊢ ( ( 1^st ↾ ran 𝐹 ) ⊆ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) → ran ( 1^st ↾ ran 𝐹 ) ⊆ ran ( 1^st ↾ ( 𝐵 × 𝐶 ) ) )
13	10 11 12	3syl	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 1^st ↾ ran 𝐹 ) ⊆ ran ( 1^st ↾ ( 𝐵 × 𝐶 ) ) )
14		f1stres	⊢ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐵
15		frn	⊢ ( ( 1^st ↾ ( 𝐵 × 𝐶 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐵 → ran ( 1^st ↾ ( 𝐵 × 𝐶 ) ) ⊆ 𝐵 )
16	14 15	ax-mp	⊢ ran ( 1^st ↾ ( 𝐵 × 𝐶 ) ) ⊆ 𝐵
17	13 16	sstrdi	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 1^st ↾ ran 𝐹 ) ⊆ 𝐵 )
18	9 17	eqsstrid	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 1^st ∘ 𝐹 ) ⊆ 𝐵 )
19		df-f	⊢ ( ( 1^st ∘ 𝐹 ) : 𝐴 ⟶ 𝐵 ↔ ( ( 1^st ∘ 𝐹 ) Fn 𝐴 ∧ ran ( 1^st ∘ 𝐹 ) ⊆ 𝐵 ) )
20	8 18 19	sylanbrc	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 1^st ∘ 𝐹 ) : 𝐴 ⟶ 𝐵 )

Metamath Proof Explorer

Theorem 1stcof

Proof