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

Metamath Proof Explorer

Theorem resdmres

Description: Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007)

Ref Expression
Assertion resdmres 
|- ( A |` dom ( A |` B ) ) = ( A |` B )

Proof

Step Hyp Ref Expression
1 in12 
 |-  ( A i^i ( ( B X. _V ) i^i ( dom A X. _V ) ) ) = ( ( B X. _V ) i^i ( A i^i ( dom A X. _V ) ) )
2 df-res 
 |-  ( A |` dom A ) = ( A i^i ( dom A X. _V ) )
3 resdm2 
 |-  ( A |` dom A ) = `' `' A
4 2 3 eqtr3i 
 |-  ( A i^i ( dom A X. _V ) ) = `' `' A
5 4 ineq2i 
 |-  ( ( B X. _V ) i^i ( A i^i ( dom A X. _V ) ) ) = ( ( B X. _V ) i^i `' `' A )
6 incom 
 |-  ( ( B X. _V ) i^i `' `' A ) = ( `' `' A i^i ( B X. _V ) )
7 1 5 6 3eqtri 
 |-  ( A i^i ( ( B X. _V ) i^i ( dom A X. _V ) ) ) = ( `' `' A i^i ( B X. _V ) )
8 df-res 
 |-  ( A |` dom ( A |` B ) ) = ( A i^i ( dom ( A |` B ) X. _V ) )
9 dmres 
 |-  dom ( A |` B ) = ( B i^i dom A )
10 9 xpeq1i 
 |-  ( dom ( A |` B ) X. _V ) = ( ( B i^i dom A ) X. _V )
11 xpindir 
 |-  ( ( B i^i dom A ) X. _V ) = ( ( B X. _V ) i^i ( dom A X. _V ) )
12 10 11 eqtri 
 |-  ( dom ( A |` B ) X. _V ) = ( ( B X. _V ) i^i ( dom A X. _V ) )
13 12 ineq2i 
 |-  ( A i^i ( dom ( A |` B ) X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( dom A X. _V ) ) )
14 8 13 eqtri 
 |-  ( A |` dom ( A |` B ) ) = ( A i^i ( ( B X. _V ) i^i ( dom A X. _V ) ) )
15 df-res 
 |-  ( `' `' A |` B ) = ( `' `' A i^i ( B X. _V ) )
16 7 14 15 3eqtr4i 
 |-  ( A |` dom ( A |` B ) ) = ( `' `' A |` B )
17 rescnvcnv 
 |-  ( `' `' A |` B ) = ( A |` B )
18 16 17 eqtri 
 |-  ( A |` dom ( A |` B ) ) = ( A |` B )