fcoresf1lem

Step	Hyp	Ref	Expression
1		fcores.f	$⊢ φ \to F : A ⟶ B$
2		fcores.e	$⊢ E = ran F \cap C$
3		fcores.p	$⊢ P = F^{-1} [C]$
4		fcores.x	$⊢ X = {F ↾}_{P}$
5		fcores.g	$⊢ φ \to G : C ⟶ D$
6		fcores.y	$⊢ Y = {G ↾}_{E}$
7	1 2 3 4 5 6	fcores	$⊢ φ \to G \circ F = Y \circ X$
8	7	fveq1d	$⊢ φ \to (G \circ F) (Z) = (Y \circ X) (Z)$
9	8	adantr	$⊢ (φ \land Z \in P) \to (G \circ F) (Z) = (Y \circ X) (Z)$
10	1 2 3 4	fcoreslem3	$⊢ φ \to X : P \underset{onto}{⟶} E$
11		fof	$⊢ X : P \underset{onto}{⟶} E \to X : P ⟶ E$
12	10 11	syl	$⊢ φ \to X : P ⟶ E$
13	12	adantr	$⊢ (φ \land Z \in P) \to X : P ⟶ E$
14		simpr	$⊢ (φ \land Z \in P) \to Z \in P$
15	13 14	fvco3d	$⊢ (φ \land Z \in P) \to (Y \circ X) (Z) = Y (X (Z))$
16	9 15	eqtrd	$⊢ (φ \land Z \in P) \to (G \circ F) (Z) = Y (X (Z))$

Metamath Proof Explorer