Theorem coiun1

Description: Composition with an indexed union. Proof analgous to that of coiun . (Contributed by RP, 20-Jun-2020)

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

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	anbi2i	⊢ ( ( 𝑦 𝐵 𝑤 ∧ 𝑤 ∪ 𝑥 ∈ 𝐶 𝐴 𝑧 ) ↔ ( 𝑦 𝐵 𝑤 ∧ ∃ 𝑥 ∈ 𝐶 𝑤 𝐴 𝑧 ) )
12		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ( 𝑦 𝐵 𝑤 ∧ ∃ 𝑥 ∈ 𝐶 𝑤 𝐴 𝑧 ) )
13	11 12	bitr4i	⊢ ( ( 𝑦 𝐵 𝑤 ∧ 𝑤 ∪ 𝑥 ∈ 𝐶 𝐴 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
14	13	exbii	⊢ ( ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 ∪ 𝑥 ∈ 𝐶 𝐴 𝑧 ) ↔ ∃ 𝑤 ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
15		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ↔ ∃ 𝑤 ∃ 𝑥 ∈ 𝐶 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
16	14 15	bitr4i	⊢ ( ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 ∪ 𝑥 ∈ 𝐶 𝐴 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
17		vex	⊢ 𝑦 ∈ V
18		vex	⊢ 𝑧 ∈ V
19	17 18	opelco	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 ∪ 𝑥 ∈ 𝐶 𝐴 𝑧 ) )
20		eliun	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) )
21	17 18	opelco	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
22	21	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐶 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
23	20 22	bitri	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑤 ( 𝑦 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) )
24	16 19 23	3bitr4i	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 ) )
25	1 5 24	eqrelriiv	⊢ ( ∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵 ) = ∪ 𝑥 ∈ 𝐶 ( 𝐴 ∘ 𝐵 )