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

Metamath Proof Explorer

Theorem imaundir

Description: The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008)

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

Proof

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