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

Metamath Proof Explorer

Theorem coundi

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

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

Proof

Step Hyp Ref Expression
1 unopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐴 𝑦 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ∨ ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) }
2 brun ⊢ ( 𝑥 ( 𝐵 ∪ 𝐶 ) 𝑧 ↔ ( 𝑥 𝐵 𝑧 ∨ 𝑥 𝐶 𝑧 ) )
3 2 anbi1i ⊢ ( ( 𝑥 ( 𝐵 ∪ 𝐶 ) 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( ( 𝑥 𝐵 𝑧 ∨ 𝑥 𝐶 𝑧 ) ∧ 𝑧 𝐴 𝑦 ) )
4 andir ⊢ ( ( ( 𝑥 𝐵 𝑧 ∨ 𝑥 𝐶 𝑧 ) ∧ 𝑧 𝐴 𝑦 ) ↔ ( ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ∨ ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
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 ⊢ ( 𝐴 ∘ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∘ 𝐵 ) ∪ ( 𝐴 ∘ 𝐶 ) )