| Step | Hyp | Ref
| Expression |
| 1 | | relco 6126 |
. 2
⊢ Rel
(∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) |
| 2 | | reliun 5826 |
. . 3
⊢ (Rel
∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) ↔ ∀𝑥 ∈ 𝐶 Rel (𝐴 ∘ 𝐵)) |
| 3 | | relco 6126 |
. . . 4
⊢ Rel
(𝐴 ∘ 𝐵) |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝑥 ∈ 𝐶 → Rel (𝐴 ∘ 𝐵)) |
| 5 | 2, 4 | mprgbir 3068 |
. 2
⊢ Rel
∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) |
| 6 | | eliun 4995 |
. . . . . . . 8
⊢
(〈𝑤, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝐶 𝐴 ↔ ∃𝑥 ∈ 𝐶 〈𝑤, 𝑧〉 ∈ 𝐴) |
| 7 | | df-br 5144 |
. . . . . . . 8
⊢ (𝑤∪ 𝑥 ∈ 𝐶 𝐴𝑧 ↔ 〈𝑤, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝐶 𝐴) |
| 8 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝑤𝐴𝑧 ↔ 〈𝑤, 𝑧〉 ∈ 𝐴) |
| 9 | 8 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐶 𝑤𝐴𝑧 ↔ ∃𝑥 ∈ 𝐶 〈𝑤, 𝑧〉 ∈ 𝐴) |
| 10 | 6, 7, 9 | 3bitr4i 303 |
. . . . . . 7
⊢ (𝑤∪ 𝑥 ∈ 𝐶 𝐴𝑧 ↔ ∃𝑥 ∈ 𝐶 𝑤𝐴𝑧) |
| 11 | 10 | anbi2i 623 |
. . . . . 6
⊢ ((𝑦𝐵𝑤 ∧ 𝑤∪ 𝑥 ∈ 𝐶 𝐴𝑧) ↔ (𝑦𝐵𝑤 ∧ ∃𝑥 ∈ 𝐶 𝑤𝐴𝑧)) |
| 12 | | r19.42v 3191 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ (𝑦𝐵𝑤 ∧ ∃𝑥 ∈ 𝐶 𝑤𝐴𝑧)) |
| 13 | 11, 12 | bitr4i 278 |
. . . . 5
⊢ ((𝑦𝐵𝑤 ∧ 𝑤∪ 𝑥 ∈ 𝐶 𝐴𝑧) ↔ ∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
| 14 | 13 | exbii 1848 |
. . . 4
⊢
(∃𝑤(𝑦𝐵𝑤 ∧ 𝑤∪ 𝑥 ∈ 𝐶 𝐴𝑧) ↔ ∃𝑤∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
| 15 | | rexcom4 3288 |
. . . 4
⊢
(∃𝑥 ∈
𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑤∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
| 16 | 14, 15 | bitr4i 278 |
. . 3
⊢
(∃𝑤(𝑦𝐵𝑤 ∧ 𝑤∪ 𝑥 ∈ 𝐶 𝐴𝑧) ↔ ∃𝑥 ∈ 𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
| 17 | | vex 3484 |
. . . 4
⊢ 𝑦 ∈ V |
| 18 | | vex 3484 |
. . . 4
⊢ 𝑧 ∈ V |
| 19 | 17, 18 | opelco 5882 |
. . 3
⊢
(〈𝑦, 𝑧〉 ∈ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) ↔ ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤∪ 𝑥 ∈ 𝐶 𝐴𝑧)) |
| 20 | | eliun 4995 |
. . . 4
⊢
(〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) ↔ ∃𝑥 ∈ 𝐶 〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵)) |
| 21 | 17, 18 | opelco 5882 |
. . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
| 22 | 21 | rexbii 3094 |
. . . 4
⊢
(∃𝑥 ∈
𝐶 〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑥 ∈ 𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
| 23 | 20, 22 | bitri 275 |
. . 3
⊢
(〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) ↔ ∃𝑥 ∈ 𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
| 24 | 16, 19, 23 | 3bitr4i 303 |
. 2
⊢
(〈𝑦, 𝑧〉 ∈ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) ↔ 〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)) |
| 25 | 1, 5, 24 | eqrelriiv 5800 |
1
⊢ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) = ∪
𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) |