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

Metamath Proof Explorer

Theorem fncofn

Description: Composition of a function with domain and a function as a function with domain. Generalization of fnco . (Contributed by AV, 17-Sep-2024)

Ref Expression
Assertion fncofn ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
2 funco ⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
3 1 2 sylan ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
4 3 funfnd ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn dom ( 𝐹 ∘ 𝐺 ) )
5 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6 5 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → dom 𝐹 = 𝐴 )
7 6 eqcomd ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → 𝐴 = dom 𝐹 )
8 7 imaeq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( ◡ 𝐺 “ 𝐴 ) = ( ◡ 𝐺 “ dom 𝐹 ) )
9 dmco ⊢ dom ( 𝐹 ∘ 𝐺 ) = ( ◡ 𝐺 “ dom 𝐹 )
10 8 9 eqtr4di ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( ◡ 𝐺 “ 𝐴 ) = dom ( 𝐹 ∘ 𝐺 ) )
11 10 fneq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ↔ ( 𝐹 ∘ 𝐺 ) Fn dom ( 𝐹 ∘ 𝐺 ) ) )
12 4 11 mpbird ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )