Theorem coiun

Description: Composition with an indexed union. (Contributed by NM, 21-Dec-2008)

	Ref	Expression
Assertion	coiun	⊢ ( 𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵 ) = ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		relco	⊢ Rel ( 𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵 )
2		reliun	⊢ ( Rel ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐶 Rel ( 𝐴 ∘ 𝐵 ) )
3		relco	⊢ Rel ( 𝐴 ∘ 𝐵 )
4	3	a1i	⊢ ( 𝑥 ∈ 𝐶 → Rel ( 𝐴 ∘ 𝐵 ) )
5	2 4	mprgbir	⊢ Rel ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 )
6		eliun	⊢ ( ⟨ 𝑦 , 𝑤 ⟩ ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ↔ ∃ 𝑥 ∈ 𝐶 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 )
7		df-br	⊢ ( 𝑦 ∪ 𝑥 ∈ 𝐶 𝐵 𝑤 ↔ ⟨ 𝑦 , 𝑤 ⟩ ∈ ∪ 𝑥 ∈ 𝐶 𝐵 )
8		df-br	⊢ ( 𝑦 𝐵 𝑤 ↔ ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 )
9	8	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐶 𝑦 𝐵 𝑤 ↔ ∃ 𝑥 ∈ 𝐶 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 )
10	6 7 9	3bitr4i	⊢ ( 𝑦 ∪ 𝑥 ∈ 𝐶 𝐵 𝑤 ↔ ∃ 𝑥 ∈ 𝐶 𝑦 𝐵 𝑤 )
11	10	anbi1i	⊢ ( ( 𝑦 ∪ 𝑥 ∈ 𝐶 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐶 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
12		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐶 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
13	11 12	bitr4i	⊢ ( ( 𝑦 ∪ 𝑥 ∈ 𝐶 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
14	13	exbii	⊢ ( ∃ 𝑤 ( 𝑦 ∪ 𝑥 ∈ 𝐶 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ∃ 𝑤 ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
15		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ∃ 𝑤 ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
16	14 15	bitr4i	⊢ ( ∃ 𝑤 ( 𝑦 ∪ 𝑥 ∈ 𝐶 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
17		vex	⊢ 𝑦 ∈ V
18		vex	⊢ 𝑧 ∈ V
19	17 18	opelco	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵 ) ↔ ∃ 𝑤 ( 𝑦 ∪ 𝑥 ∈ 𝐶 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
20	17 18	opelco	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
21	20	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐶 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
22	16 19 21	3bitr4i	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) )
23		eliun	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) )
24	22 23	bitr4i	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 ) )
25	1 5 24	eqrelriiv	⊢ ( 𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵 ) = ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 )