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	$⊢ (({F ↾}_{B}) : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : A ⟶ C$

Proof

Step	Hyp	Ref	Expression
1		fco	$⊢ (({F ↾}_{B}) : B ⟶ C \land G : A ⟶ B) \to (({F ↾}_{B}) \circ G) : A ⟶ C$
2		frn	$⊢ G : A ⟶ B \to ran G \subseteq B$
3		cores	$⊢ ran G \subseteq B \to ({F ↾}_{B}) \circ G = F \circ G$
4	2 3	syl	$⊢ G : A ⟶ B \to ({F ↾}_{B}) \circ G = F \circ G$
5	4	adantl	$⊢ (({F ↾}_{B}) : B ⟶ C \land G : A ⟶ B) \to ({F ↾}_{B}) \circ G = F \circ G$
6	5	feq1d	$⊢ (({F ↾}_{B}) : B ⟶ C \land G : A ⟶ B) \to ((({F ↾}_{B}) \circ G) : A ⟶ C \leftrightarrow (F \circ G) : A ⟶ C)$
7	1 6	mpbid	$⊢ (({F ↾}_{B}) : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : A ⟶ C$