This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 × 𝐵 ) )