This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )