Theorem cores

Description: Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	cores	$$⊢\mathrm{ran}B\subseteq C\to \left({A\upharpoonright }_C\right)\circ B=A\circ B$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢z\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3	1 2	brelrn	$$⊢zBy\to y\in \mathrm{ran}B$$
4		ssel	$$⊢\mathrm{ran}B\subseteq C\to \left(y\in \mathrm{ran}B\to y\in C\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	brresi	$$⊢y\left({A\upharpoonright }_C\right)x\leftrightarrow \left(y\in C\wedge yAx\right)$$
7	6	baib	$$⊢y\in C\to \left(y\left({A\upharpoonright }_C\right)x\leftrightarrow yAx\right)$$
8	3 4 7	syl56	$$⊢\mathrm{ran}B\subseteq C\to \left(zBy\to \left(y\left({A\upharpoonright }_C\right)x\leftrightarrow yAx\right)\right)$$
9	8	pm5.32d	$$⊢\mathrm{ran}B\subseteq C\to \left(\left(zBy\wedge y\left({A\upharpoonright }_C\right)x\right)\leftrightarrow \left(zBy\wedge yAx\right)\right)$$
10	9	exbidv	$$⊢\mathrm{ran}B\subseteq C\to \left(\exists y\left(zBy\wedge y\left({A\upharpoonright }_C\right)x\right)\leftrightarrow \exists y\left(zBy\wedge yAx\right)\right)$$
11	10	opabbidv	$$⊢\mathrm{ran}B\subseteq C\to \left\{⟨z,x⟩|\exists y\left(zBy\wedge y\left({A\upharpoonright }_C\right)x\right)\right\}=\left\{⟨z,x⟩|\exists y\left(zBy\wedge yAx\right)\right\}$$
12		df-co	$$⊢\left({A\upharpoonright }_C\right)\circ B=\left\{⟨z,x⟩|\exists y\left(zBy\wedge y\left({A\upharpoonright }_C\right)x\right)\right\}$$
13		df-co	$$⊢A\circ B=\left\{⟨z,x⟩|\exists y\left(zBy\wedge yAx\right)\right\}$$
14	11 12 13	3eqtr4g	$$⊢\mathrm{ran}B\subseteq C\to \left({A\upharpoonright }_C\right)\circ B=A\circ B$$