Theorem fco2

Description: Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015)

	Ref	Expression
Assertion	fco2	⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fco	⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )
2		frn	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ran 𝐺 ⊆ 𝐵 )
3		cores	⊢ ( ran 𝐺 ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
4	2 3	syl	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
5	4	adantl	⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
6	5	feq1d	⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ) )
7	1 6	mpbid	⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )