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

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 ⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )