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

Metamath Proof Explorer

Theorem resres

Description: The restriction of a restriction. (Contributed by NM, 27-Mar-2008)

Ref Expression
Assertion resres ( ( 𝐴 ↾ 𝐵 ) ↾ 𝐶 ) = ( 𝐴 ↾ ( 𝐵 ∩ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( ( 𝐴 ↾ 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 ↾ 𝐵 ) ∩ ( 𝐶 × V ) )
2 df-res ⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
3 2 ineq1i ⊢ ( ( 𝐴 ↾ 𝐵 ) ∩ ( 𝐶 × V ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∩ ( 𝐶 × V ) )
4 xpindir ⊢ ( ( 𝐵 ∩ 𝐶 ) × V ) = ( ( 𝐵 × V ) ∩ ( 𝐶 × V ) )
5 4 ineq2i ⊢ ( 𝐴 ∩ ( ( 𝐵 ∩ 𝐶 ) × V ) ) = ( 𝐴 ∩ ( ( 𝐵 × V ) ∩ ( 𝐶 × V ) ) )
6 df-res ⊢ ( 𝐴 ↾ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐴 ∩ ( ( 𝐵 ∩ 𝐶 ) × V ) )
7 inass ⊢ ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∩ ( 𝐶 × V ) ) = ( 𝐴 ∩ ( ( 𝐵 × V ) ∩ ( 𝐶 × V ) ) )
8 5 6 7 3eqtr4ri ⊢ ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∩ ( 𝐶 × V ) ) = ( 𝐴 ↾ ( 𝐵 ∩ 𝐶 ) )
9 1 3 8 3eqtri ⊢ ( ( 𝐴 ↾ 𝐵 ) ↾ 𝐶 ) = ( 𝐴 ↾ ( 𝐵 ∩ 𝐶 ) )