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 
|- `' ( `' R |` B ) = ( R i^i ( _V X. B ) )

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( `' R |` B ) = ( `' R i^i ( B X. _V ) )
2 1 cnveqi 
 |-  `' ( `' R |` B ) = `' ( `' R i^i ( B X. _V ) )
3 cnvin 
 |-  `' ( `' R i^i ( B X. _V ) ) = ( `' `' R i^i `' ( B X. _V ) )
4 cnvcnv 
 |-  `' `' R = ( R i^i ( _V X. _V ) )
5 cnvxp 
 |-  `' ( B X. _V ) = ( _V X. B )
6 4 5 ineq12i 
 |-  ( `' `' R i^i `' ( B X. _V ) ) = ( ( R i^i ( _V X. _V ) ) i^i ( _V X. B ) )
7 inass 
 |-  ( ( R i^i ( _V X. _V ) ) i^i ( _V X. B ) ) = ( R i^i ( ( _V X. _V ) i^i ( _V X. B ) ) )
8 inxp 
 |-  ( ( _V X. _V ) i^i ( _V X. B ) ) = ( ( _V i^i _V ) X. ( _V i^i B ) )
9 inv1 
 |-  ( _V i^i _V ) = _V
10 9 eqcomi 
 |-  _V = ( _V i^i _V )
11 ssv 
 |-  B C_ _V
12 ssid 
 |-  B C_ B
13 11 12 ssini 
 |-  B C_ ( _V i^i B )
14 inss2 
 |-  ( _V i^i B ) C_ B
15 13 14 eqssi 
 |-  B = ( _V i^i B )
16 10 15 xpeq12i 
 |-  ( _V X. B ) = ( ( _V i^i _V ) X. ( _V i^i B ) )
17 8 16 eqtr4i 
 |-  ( ( _V X. _V ) i^i ( _V X. B ) ) = ( _V X. B )
18 17 ineq2i 
 |-  ( R i^i ( ( _V X. _V ) i^i ( _V X. B ) ) ) = ( R i^i ( _V X. B ) )
19 6 7 18 3eqtri 
 |-  ( `' `' R i^i `' ( B X. _V ) ) = ( R i^i ( _V X. B ) )
20 2 3 19 3eqtri 
 |-  `' ( `' R |` B ) = ( R i^i ( _V X. B ) )