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 )