Metamath Proof Explorer

Theorem coiun1

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

Ref Expression
Assertion coiun1 ⊢⋃x∈CA∘B=⋃x∈CA∘B

Proof

Step Hyp Ref Expression
1 relco ⊢Rel⁡⋃x∈CA∘B
2 reliun ⊢Rel⁡⋃x∈CA∘B↔∀x∈CRel⁡A∘B
3 relco ⊢Rel⁡A∘B
4 3 a1i ⊢x∈C→Rel⁡A∘B
5 2 4 mprgbir ⊢Rel⁡⋃x∈CA∘B
6 eliun ⊢wz∈⋃x∈CA↔∃x∈Cwz∈A
7 df-br ⊢w⋃x∈CAz↔wz∈⋃x∈CA
8 df-br ⊢wAz↔wz∈A
9 8 rexbii ⊢∃x∈CwAz↔∃x∈Cwz∈A
10 6 7 9 3bitr4i ⊢w⋃x∈CAz↔∃x∈CwAz
11 10 anbi2i ⊢yBw∧w⋃x∈CAz↔yBw∧∃x∈CwAz
12 r19.42v ⊢∃x∈CyBw∧wAz↔yBw∧∃x∈CwAz
13 11 12 bitr4i ⊢yBw∧w⋃x∈CAz↔∃x∈CyBw∧wAz
14 13 exbii ⊢∃wyBw∧w⋃x∈CAz↔∃w∃x∈CyBw∧wAz
15 rexcom4 ⊢∃x∈C∃wyBw∧wAz↔∃w∃x∈CyBw∧wAz
16 14 15 bitr4i ⊢∃wyBw∧w⋃x∈CAz↔∃x∈C∃wyBw∧wAz
17 vex ⊢y∈V
18 vex ⊢z∈V
19 17 18 opelco ⊢yz∈⋃x∈CA∘B↔∃wyBw∧w⋃x∈CAz
20 eliun ⊢yz∈⋃x∈CA∘B↔∃x∈Cyz∈A∘B
21 17 18 opelco ⊢yz∈A∘B↔∃wyBw∧wAz
22 21 rexbii ⊢∃x∈Cyz∈A∘B↔∃x∈C∃wyBw∧wAz
23 20 22 bitri ⊢yz∈⋃x∈CA∘B↔∃x∈C∃wyBw∧wAz
24 16 19 23 3bitr4i ⊢yz∈⋃x∈CA∘B↔yz∈⋃x∈CA∘B
25 1 5 24 eqrelriiv ⊢⋃x∈CA∘B=⋃x∈CA∘B