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 ( 𝐴 ↾ 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 ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 )