Theorem fco

Description: Composition of two functions with domain and codomain as a function with domain and codomain. (Contributed by NM, 29-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Proof shortened by AV, 20-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ffun	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → Fun 𝐺 )
2		fcof	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) ⟶ 𝐶 )
3	1 2	sylan2	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) ⟶ 𝐶 )
4		fimacnv	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐺 “ 𝐵 ) = 𝐴 )
5	4	eqcomd	⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → 𝐴 = ( ◡ 𝐺 “ 𝐵 ) )
6	5	adantl	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → 𝐴 = ( ◡ 𝐺 “ 𝐵 ) )
7	6	feq2d	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐵 ) ⟶ 𝐶 ) )
8	3 7	mpbird	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )