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

Metamath Proof Explorer

Theorem fnco

Description: Composition of two functions with domains as a function with domain. (Contributed by NM, 22-May-2006) (Proof shortened by AV, 20-Sep-2024)

Ref Expression
Assertion fnco ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )

Proof

Step Hyp Ref Expression
1 fnfun ⊢ ( 𝐺 Fn 𝐵 → Fun 𝐺 )
2 fncofn ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )
3 1 2 sylan2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )
4 3 3adant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )
5 cnvimassrndm ⊢ ( ran 𝐺 ⊆ 𝐴 → ( ◡ 𝐺 “ 𝐴 ) = dom 𝐺 )
6 5 3ad2ant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( ◡ 𝐺 “ 𝐴 ) = dom 𝐺 )
7 fndm ⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
8 7 3ad2ant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → dom 𝐺 = 𝐵 )
9 6 8 eqtr2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → 𝐵 = ( ◡ 𝐺 “ 𝐴 ) )
10 9 fneq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) Fn 𝐵 ↔ ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ) )
11 4 10 mpbird ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )