Theorem coires2

Description: Postcomposing with a restricted identity relation is the same as corestricting. (Contributed by BJ, 1-Nov-2026)

	Ref	Expression
Assertion	coires2	⊢ ( ( I ↾ 𝐵 ) ∘ 𝐴 ) = ( 𝐴 ∩ ( V × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cnvresid	⊢ ◡ ( I ↾ 𝐵 ) = ( I ↾ 𝐵 )
2	1	coeq1i	⊢ ( ◡ ( I ↾ 𝐵 ) ∘ ◡ ◡ 𝐴 ) = ( ( I ↾ 𝐵 ) ∘ ◡ ◡ 𝐴 )
3		coires1	⊢ ( ◡ 𝐴 ∘ ( I ↾ 𝐵 ) ) = ( ◡ 𝐴 ↾ 𝐵 )
4	3	cnveqi	⊢ ◡ ( ◡ 𝐴 ∘ ( I ↾ 𝐵 ) ) = ◡ ( ◡ 𝐴 ↾ 𝐵 )
5		cnvco	⊢ ◡ ( ◡ 𝐴 ∘ ( I ↾ 𝐵 ) ) = ( ◡ ( I ↾ 𝐵 ) ∘ ◡ ◡ 𝐴 )
6		cnvrescnv	⊢ ◡ ( ◡ 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( V × 𝐵 ) )
7	4 5 6	3eqtr3i	⊢ ( ◡ ( I ↾ 𝐵 ) ∘ ◡ ◡ 𝐴 ) = ( 𝐴 ∩ ( V × 𝐵 ) )
8		cocnvcnv2	⊢ ( ( I ↾ 𝐵 ) ∘ ◡ ◡ 𝐴 ) = ( ( I ↾ 𝐵 ) ∘ 𝐴 )
9	2 7 8	3eqtr3ri	⊢ ( ( I ↾ 𝐵 ) ∘ 𝐴 ) = ( 𝐴 ∩ ( V × 𝐵 ) )