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	⊢ ( 𝐴 ∘ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∘ 𝐵 ) ∪ ( 𝐴 ∘ 𝐶 ) )