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 
|- ( ( F : A --> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )

Proof

Step Hyp Ref Expression
1 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2 fncofn 
 |-  ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn ( `' G " A ) )
3 2 ex 
 |-  ( F Fn A -> ( Fun G -> ( F o. G ) Fn ( `' G " A ) ) )
4 3 adantr 
 |-  ( ( F Fn A /\ ran F C_ B ) -> ( Fun G -> ( F o. G ) Fn ( `' G " A ) ) )
5 rncoss 
 |-  ran ( F o. G ) C_ ran F
6 sstr 
 |-  ( ( ran ( F o. G ) C_ ran F /\ ran F C_ B ) -> ran ( F o. G ) C_ B )
7 5 6 mpan 
 |-  ( ran F C_ B -> ran ( F o. G ) C_ B )
8 7 adantl 
 |-  ( ( F Fn A /\ ran F C_ B ) -> ran ( F o. G ) C_ B )
9 4 8 jctird 
 |-  ( ( F Fn A /\ ran F C_ B ) -> ( Fun G -> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) ) )
10 9 imp 
 |-  ( ( ( F Fn A /\ ran F C_ B ) /\ Fun G ) -> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) )
11 1 10 sylanb 
 |-  ( ( F : A --> B /\ Fun G ) -> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) )
12 df-f 
 |-  ( ( F o. G ) : ( `' G " A ) --> B <-> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) )
13 11 12 sylibr 
 |-  ( ( F : A --> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )