Theorem resdmres

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

	Ref	Expression
Assertion	resdmres	⊢ ( 𝐴 ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		in12	⊢ ( 𝐴 ∩ ( ( 𝐵 × V ) ∩ ( dom 𝐴 × V ) ) ) = ( ( 𝐵 × V ) ∩ ( 𝐴 ∩ ( dom 𝐴 × V ) ) )
2		df-res	⊢ ( 𝐴 ↾ dom 𝐴 ) = ( 𝐴 ∩ ( dom 𝐴 × V ) )
3		resdm2	⊢ ( 𝐴 ↾ dom 𝐴 ) = ◡ ◡ 𝐴
4	2 3	eqtr3i	⊢ ( 𝐴 ∩ ( dom 𝐴 × V ) ) = ◡ ◡ 𝐴
5	4	ineq2i	⊢ ( ( 𝐵 × V ) ∩ ( 𝐴 ∩ ( dom 𝐴 × V ) ) ) = ( ( 𝐵 × V ) ∩ ◡ ◡ 𝐴 )
6		incom	⊢ ( ( 𝐵 × V ) ∩ ◡ ◡ 𝐴 ) = ( ◡ ◡ 𝐴 ∩ ( 𝐵 × V ) )
7	1 5 6	3eqtri	⊢ ( 𝐴 ∩ ( ( 𝐵 × V ) ∩ ( dom 𝐴 × V ) ) ) = ( ◡ ◡ 𝐴 ∩ ( 𝐵 × V ) )
8		df-res	⊢ ( 𝐴 ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ∩ ( dom ( 𝐴 ↾ 𝐵 ) × V ) )
9		dmres	⊢ dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 )
10	9	xpeq1i	⊢ ( dom ( 𝐴 ↾ 𝐵 ) × V ) = ( ( 𝐵 ∩ dom 𝐴 ) × V )
11		xpindir	⊢ ( ( 𝐵 ∩ dom 𝐴 ) × V ) = ( ( 𝐵 × V ) ∩ ( dom 𝐴 × V ) )
12	10 11	eqtri	⊢ ( dom ( 𝐴 ↾ 𝐵 ) × V ) = ( ( 𝐵 × V ) ∩ ( dom 𝐴 × V ) )
13	12	ineq2i	⊢ ( 𝐴 ∩ ( dom ( 𝐴 ↾ 𝐵 ) × V ) ) = ( 𝐴 ∩ ( ( 𝐵 × V ) ∩ ( dom 𝐴 × V ) ) )
14	8 13	eqtri	⊢ ( 𝐴 ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ∩ ( ( 𝐵 × V ) ∩ ( dom 𝐴 × V ) ) )
15		df-res	⊢ ( ◡ ◡ 𝐴 ↾ 𝐵 ) = ( ◡ ◡ 𝐴 ∩ ( 𝐵 × V ) )
16	7 14 15	3eqtr4i	⊢ ( 𝐴 ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( ◡ ◡ 𝐴 ↾ 𝐵 )
17		rescnvcnv	⊢ ( ◡ ◡ 𝐴 ↾ 𝐵 ) = ( 𝐴 ↾ 𝐵 )
18	16 17	eqtri	⊢ ( 𝐴 ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 )