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 )