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

Metamath Proof Explorer

Theorem resundi

Description: Distributive law for restriction over union. Theorem 31 of Suppes p. 65. (Contributed by NM, 30-Sep-2002)

Ref Expression
Assertion resundi ( 𝐴 ↾ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ↾ 𝐵 ) ∪ ( 𝐴 ↾ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 xpundir ⊢ ( ( 𝐵 ∪ 𝐶 ) × V ) = ( ( 𝐵 × V ) ∪ ( 𝐶 × V ) )
2 1 ineq2i ⊢ ( 𝐴 ∩ ( ( 𝐵 ∪ 𝐶 ) × V ) ) = ( 𝐴 ∩ ( ( 𝐵 × V ) ∪ ( 𝐶 × V ) ) )
3 indi ⊢ ( 𝐴 ∩ ( ( 𝐵 × V ) ∪ ( 𝐶 × V ) ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∪ ( 𝐴 ∩ ( 𝐶 × V ) ) )
4 2 3 eqtri ⊢ ( 𝐴 ∩ ( ( 𝐵 ∪ 𝐶 ) × V ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∪ ( 𝐴 ∩ ( 𝐶 × V ) ) )
5 df-res ⊢ ( 𝐴 ↾ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐴 ∩ ( ( 𝐵 ∪ 𝐶 ) × V ) )
6 df-res ⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
7 df-res ⊢ ( 𝐴 ↾ 𝐶 ) = ( 𝐴 ∩ ( 𝐶 × V ) )
8 6 7 uneq12i ⊢ ( ( 𝐴 ↾ 𝐵 ) ∪ ( 𝐴 ↾ 𝐶 ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∪ ( 𝐴 ∩ ( 𝐶 × V ) ) )
9 4 5 8 3eqtr4i ⊢ ( 𝐴 ↾ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ↾ 𝐵 ) ∪ ( 𝐴 ↾ 𝐶 ) )