Theorem cnvrescnv

Description: Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023)

	Ref	Expression
Assertion	cnvrescnv	⊢ ◡ ( ◡ 𝑅 ↾ 𝐵 ) = ( 𝑅 ∩ ( V × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( ◡ 𝑅 ↾ 𝐵 ) = ( ◡ 𝑅 ∩ ( 𝐵 × V ) )
2	1	cnveqi	⊢ ◡ ( ◡ 𝑅 ↾ 𝐵 ) = ◡ ( ◡ 𝑅 ∩ ( 𝐵 × V ) )
3		cnvin	⊢ ◡ ( ◡ 𝑅 ∩ ( 𝐵 × V ) ) = ( ◡ ◡ 𝑅 ∩ ◡ ( 𝐵 × V ) )
4		cnvcnv	⊢ ◡ ◡ 𝑅 = ( 𝑅 ∩ ( V × V ) )
5		cnvxp	⊢ ◡ ( 𝐵 × V ) = ( V × 𝐵 )
6	4 5	ineq12i	⊢ ( ◡ ◡ 𝑅 ∩ ◡ ( 𝐵 × V ) ) = ( ( 𝑅 ∩ ( V × V ) ) ∩ ( V × 𝐵 ) )
7		inass	⊢ ( ( 𝑅 ∩ ( V × V ) ) ∩ ( V × 𝐵 ) ) = ( 𝑅 ∩ ( ( V × V ) ∩ ( V × 𝐵 ) ) )
8		inxp	⊢ ( ( V × V ) ∩ ( V × 𝐵 ) ) = ( ( V ∩ V ) × ( V ∩ 𝐵 ) )
9		inv1	⊢ ( V ∩ V ) = V
10	9	eqcomi	⊢ V = ( V ∩ V )
11		ssv	⊢ 𝐵 ⊆ V
12		ssid	⊢ 𝐵 ⊆ 𝐵
13	11 12	ssini	⊢ 𝐵 ⊆ ( V ∩ 𝐵 )
14		inss2	⊢ ( V ∩ 𝐵 ) ⊆ 𝐵
15	13 14	eqssi	⊢ 𝐵 = ( V ∩ 𝐵 )
16	10 15	xpeq12i	⊢ ( V × 𝐵 ) = ( ( V ∩ V ) × ( V ∩ 𝐵 ) )
17	8 16	eqtr4i	⊢ ( ( V × V ) ∩ ( V × 𝐵 ) ) = ( V × 𝐵 )
18	17	ineq2i	⊢ ( 𝑅 ∩ ( ( V × V ) ∩ ( V × 𝐵 ) ) ) = ( 𝑅 ∩ ( V × 𝐵 ) )
19	6 7 18	3eqtri	⊢ ( ◡ ◡ 𝑅 ∩ ◡ ( 𝐵 × V ) ) = ( 𝑅 ∩ ( V × 𝐵 ) )
20	2 3 19	3eqtri	⊢ ◡ ( ◡ 𝑅 ↾ 𝐵 ) = ( 𝑅 ∩ ( V × 𝐵 ) )