Theorem 2ndcof

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

	Ref	Expression
Assertion	2ndcof	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 2nd ∘ 𝐹 ) : 𝐴 ⟶ 𝐶 )

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	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → 𝐹 Fn 𝐴 )
5		dffn2	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ V )
6	4 5	sylib	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → 𝐹 : 𝐴 ⟶ V )
7		fnfco	⊢ ( ( 2nd Fn V ∧ 𝐹 : 𝐴 ⟶ V ) → ( 2nd ∘ 𝐹 ) Fn 𝐴 )
8	3 6 7	sylancr	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 2nd ∘ 𝐹 ) Fn 𝐴 )
9		rnco	⊢ ran ( 2nd ∘ 𝐹 ) = ran ( 2nd ↾ ran 𝐹 )
10		frn	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran 𝐹 ⊆ ( 𝐵 × 𝐶 ) )
11		ssres2	⊢ ( ran 𝐹 ⊆ ( 𝐵 × 𝐶 ) → ( 2nd ↾ ran 𝐹 ) ⊆ ( 2nd ↾ ( 𝐵 × 𝐶 ) ) )
12		rnss	⊢ ( ( 2nd ↾ ran 𝐹 ) ⊆ ( 2nd ↾ ( 𝐵 × 𝐶 ) ) → ran ( 2nd ↾ ran 𝐹 ) ⊆ ran ( 2nd ↾ ( 𝐵 × 𝐶 ) ) )
13	10 11 12	3syl	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 2nd ↾ ran 𝐹 ) ⊆ ran ( 2nd ↾ ( 𝐵 × 𝐶 ) ) )
14		f2ndres	⊢ ( 2nd ↾ ( 𝐵 × 𝐶 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐶
15		frn	⊢ ( ( 2nd ↾ ( 𝐵 × 𝐶 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐶 → ran ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ⊆ 𝐶 )
16	14 15	ax-mp	⊢ ran ( 2nd ↾ ( 𝐵 × 𝐶 ) ) ⊆ 𝐶
17	13 16	sstrdi	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 2nd ↾ ran 𝐹 ) ⊆ 𝐶 )
18	9 17	eqsstrid	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 2nd ∘ 𝐹 ) ⊆ 𝐶 )
19		df-f	⊢ ( ( 2nd ∘ 𝐹 ) : 𝐴 ⟶ 𝐶 ↔ ( ( 2nd ∘ 𝐹 ) Fn 𝐴 ∧ ran ( 2nd ∘ 𝐹 ) ⊆ 𝐶 ) )
20	8 18 19	sylanbrc	⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 2nd ∘ 𝐹 ) : 𝐴 ⟶ 𝐶 )