Metamath Proof Explorer


Theorem fco2

Description: Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015)

Ref Expression
Assertion fco2 ( ( ( 𝐹𝐵 ) : 𝐵𝐶𝐺 : 𝐴𝐵 ) → ( 𝐹𝐺 ) : 𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 fco ( ( ( 𝐹𝐵 ) : 𝐵𝐶𝐺 : 𝐴𝐵 ) → ( ( 𝐹𝐵 ) ∘ 𝐺 ) : 𝐴𝐶 )
2 frn ( 𝐺 : 𝐴𝐵 → ran 𝐺𝐵 )
3 cores ( ran 𝐺𝐵 → ( ( 𝐹𝐵 ) ∘ 𝐺 ) = ( 𝐹𝐺 ) )
4 2 3 syl ( 𝐺 : 𝐴𝐵 → ( ( 𝐹𝐵 ) ∘ 𝐺 ) = ( 𝐹𝐺 ) )
5 4 adantl ( ( ( 𝐹𝐵 ) : 𝐵𝐶𝐺 : 𝐴𝐵 ) → ( ( 𝐹𝐵 ) ∘ 𝐺 ) = ( 𝐹𝐺 ) )
6 5 feq1d ( ( ( 𝐹𝐵 ) : 𝐵𝐶𝐺 : 𝐴𝐵 ) → ( ( ( 𝐹𝐵 ) ∘ 𝐺 ) : 𝐴𝐶 ↔ ( 𝐹𝐺 ) : 𝐴𝐶 ) )
7 1 6 mpbid ( ( ( 𝐹𝐵 ) : 𝐵𝐶𝐺 : 𝐴𝐵 ) → ( 𝐹𝐺 ) : 𝐴𝐶 )