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 𝐵 )