Theorem coresrn

Description: When composing classes, restricting the second class to the range of the first has no effect. (Contributed by BJ, 22-Oct-2026) Note: can be moved before cores and shorten funresfunco , dprdf1 , kgencn2 , domss2 .

	Ref	Expression
Assertion	coresrn	|- ( ( B |` ran A ) o. A ) = ( B o. A )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		vex	|- y e. _V
3	1 2	brelrn	|- ( x A y -> y e. ran A )
4		vex	|- z e. _V
5	4	brresi	|- ( y ( B |` ran A ) z <-> ( y e. ran A /\ y B z ) )
6	5	baib	|- ( y e. ran A -> ( y ( B |` ran A ) z <-> y B z ) )
7	3 6	syl	|- ( x A y -> ( y ( B |` ran A ) z <-> y B z ) )
8	7	pm5.32i	|- ( ( x A y /\ y ( B |` ran A ) z ) <-> ( x A y /\ y B z ) )
9	8	exbii	|- ( E. y ( x A y /\ y ( B |` ran A ) z ) <-> E. y ( x A y /\ y B z ) )
10	9	opabbii	|- { <. x , z >. | E. y ( x A y /\ y ( B |` ran A ) z ) } = { <. x , z >. | E. y ( x A y /\ y B z ) }
11		df-co	|- ( ( B |` ran A ) o. A ) = { <. x , z >. | E. y ( x A y /\ y ( B |` ran A ) z ) }
12		df-co	|- ( B o. A ) = { <. x , z >. | E. y ( x A y /\ y B z ) }
13	10 11 12	3eqtr4i	|- ( ( B |` ran A ) o. A ) = ( B o. A )