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

Metamath Proof Explorer

Theorem fcof

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

Ref Expression
Assertion fcof ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
2 fncofn ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) )
3 2 ex ⊢ ( 𝐹 Fn 𝐴 → ( Fun 𝐺 → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ) )
4 3 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ( Fun 𝐺 → ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ) )
5 rncoss ⊢ ran ( 𝐹 ∘ 𝐺 ) ⊆ ran 𝐹
6 sstr ⊢ ( ( ran ( 𝐹 ∘ 𝐺 ) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 )
7 5 6 mpan ⊢ ( ran 𝐹 ⊆ 𝐵 → ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 )
8 7 adantl ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 )
9 4 8 jctird ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ( Fun 𝐺 → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) ) )
10 9 imp ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) )
11 1 10 sylanb ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) )
12 df-f ⊢ ( ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 ↔ ( ( 𝐹 ∘ 𝐺 ) Fn ( ◡ 𝐺 “ 𝐴 ) ∧ ran ( 𝐹 ∘ 𝐺 ) ⊆ 𝐵 ) )
13 11 12 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 )