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