This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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