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

Metamath Proof Explorer

Theorem coundir

Description: Class composition distributes over union. (Contributed by NM, 21-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion coundir ( ( 𝐴 ∪ 𝐵 ) ∘ 𝐶 ) = ( ( 𝐴 ∘ 𝐶 ) ∪ ( 𝐵 ∘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 unopab ⊢ ( { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) } ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) }
2 brun ⊢ ( 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ↔ ( 𝑦 𝐴 𝑧 ∨ 𝑦 𝐵 𝑧 ) )
3 2 anbi2i ⊢ ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ) ↔ ( 𝑥 𝐶 𝑦 ∧ ( 𝑦 𝐴 𝑧 ∨ 𝑦 𝐵 𝑧 ) ) )
4 andi ⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑦 𝐴 𝑧 ∨ 𝑦 𝐵 𝑧 ) ) ↔ ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) )
5 3 4 bitri ⊢ ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ) ↔ ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ) ↔ ∃ 𝑦 ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) )
7 19.43 ⊢ ( ∃ 𝑦 ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) ↔ ( ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) )
8 6 7 bitr2i ⊢ ( ( ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) ↔ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ) )
9 8 opabbii ⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∨ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ) }
10 1 9 eqtri ⊢ ( { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) } ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ) }
11 df-co ⊢ ( 𝐴 ∘ 𝐶 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) }
12 df-co ⊢ ( 𝐵 ∘ 𝐶 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) }
13 11 12 uneq12i ⊢ ( ( 𝐴 ∘ 𝐶 ) ∪ ( 𝐵 ∘ 𝐶 ) ) = ( { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) } ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐵 𝑧 ) } )
14 df-co ⊢ ( ( 𝐴 ∪ 𝐵 ) ∘ 𝐶 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 ( 𝐴 ∪ 𝐵 ) 𝑧 ) }
15 10 13 14 3eqtr4ri ⊢ ( ( 𝐴 ∪ 𝐵 ) ∘ 𝐶 ) = ( ( 𝐴 ∘ 𝐶 ) ∪ ( 𝐵 ∘ 𝐶 ) )