Metamath Proof Explorer


Theorem imaundi

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

Ref Expression
Assertion imaundi ( 𝐴 “ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐶 ) )

Proof

Step Hyp Ref Expression
1 resundi ( 𝐴 ↾ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐶 ) )
2 1 rneqi ran ( 𝐴 ↾ ( 𝐵𝐶 ) ) = ran ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐶 ) )
3 rnun ran ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐶 ) ) = ( ran ( 𝐴𝐵 ) ∪ ran ( 𝐴𝐶 ) )
4 2 3 eqtri ran ( 𝐴 ↾ ( 𝐵𝐶 ) ) = ( ran ( 𝐴𝐵 ) ∪ ran ( 𝐴𝐶 ) )
5 df-ima ( 𝐴 “ ( 𝐵𝐶 ) ) = ran ( 𝐴 ↾ ( 𝐵𝐶 ) )
6 df-ima ( 𝐴𝐵 ) = ran ( 𝐴𝐵 )
7 df-ima ( 𝐴𝐶 ) = ran ( 𝐴𝐶 )
8 6 7 uneq12i ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐶 ) ) = ( ran ( 𝐴𝐵 ) ∪ ran ( 𝐴𝐶 ) )
9 4 5 8 3eqtr4i ( 𝐴 “ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐶 ) )