Metamath Proof Explorer

Theorem fco3OLD

Description: Obsolete version of funcofd as 20-Sep-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	fco3OLD.1	$⊢ φ \to Fun F$
		fco3OLD.2	$⊢ φ \to Fun G$
	Assertion	fco3OLD	$⊢ φ \to (F \circ G) : G^{-1} [dom F] ⟶ ran F$

Proof

Step	Hyp	Ref	Expression
1		fco3OLD.1	$⊢ φ \to Fun F$
2		fco3OLD.2	$⊢ φ \to Fun G$
3		funco	$⊢ (Fun F \land Fun G) \to Fun (F \circ G)$
4	1 2 3	syl2anc	$⊢ φ \to Fun (F \circ G)$
5		fdmrn	$⊢ Fun (F \circ G) \leftrightarrow (F \circ G) : dom (F \circ G) ⟶ ran (F \circ G)$
6	4 5	sylib	$⊢ φ \to (F \circ G) : dom (F \circ G) ⟶ ran (F \circ G)$
7		dmco	$⊢ dom (F \circ G) = G^{-1} [dom F]$
8	7	feq2i	$⊢ (F \circ G) : dom (F \circ G) ⟶ ran (F \circ G) \leftrightarrow (F \circ G) : G^{-1} [dom F] ⟶ ran (F \circ G)$
9	6 8	sylib	$⊢ φ \to (F \circ G) : G^{-1} [dom F] ⟶ ran (F \circ G)$
10		rncoss	$⊢ ran (F \circ G) \subseteq ran F$
11	10	a1i	$⊢ φ \to ran (F \circ G) \subseteq ran F$
12	9 11	fssd	$⊢ φ \to (F \circ G) : G^{-1} [dom F] ⟶ ran F$