Step | Hyp | Ref
| Expression |
1 | | relco 6148 |
. 2
⊢ Rel
(𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) |
2 | | reliun 5726 |
. . 3
⊢ (Rel
∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) ↔ ∀𝑥 ∈ 𝐶 Rel (𝐴 ∘ 𝐵)) |
3 | | relco 6148 |
. . . 4
⊢ Rel
(𝐴 ∘ 𝐵) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝑥 ∈ 𝐶 → Rel (𝐴 ∘ 𝐵)) |
5 | 2, 4 | mprgbir 3079 |
. 2
⊢ Rel
∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) |
6 | | eliun 4928 |
. . . . . . . . 9
⊢
(〈𝑦, 𝑤〉 ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ↔ ∃𝑥 ∈ 𝐶 〈𝑦, 𝑤〉 ∈ 𝐵) |
7 | | df-br 5075 |
. . . . . . . . 9
⊢ (𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ↔ 〈𝑦, 𝑤〉 ∈ ∪ 𝑥 ∈ 𝐶 𝐵) |
8 | | df-br 5075 |
. . . . . . . . . 10
⊢ (𝑦𝐵𝑤 ↔ 〈𝑦, 𝑤〉 ∈ 𝐵) |
9 | 8 | rexbii 3181 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐶 𝑦𝐵𝑤 ↔ ∃𝑥 ∈ 𝐶 〈𝑦, 𝑤〉 ∈ 𝐵) |
10 | 6, 7, 9 | 3bitr4i 303 |
. . . . . . . 8
⊢ (𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ↔ ∃𝑥 ∈ 𝐶 𝑦𝐵𝑤) |
11 | 10 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ (∃𝑥 ∈ 𝐶 𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
12 | | r19.41v 3276 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ (∃𝑥 ∈ 𝐶 𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
13 | 11, 12 | bitr4i 277 |
. . . . . 6
⊢ ((𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
14 | 13 | exbii 1850 |
. . . . 5
⊢
(∃𝑤(𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑤∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
15 | | rexcom4 3233 |
. . . . 5
⊢
(∃𝑥 ∈
𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑤∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
16 | 14, 15 | bitr4i 277 |
. . . 4
⊢
(∃𝑤(𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑥 ∈ 𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
17 | | vex 3436 |
. . . . 5
⊢ 𝑦 ∈ V |
18 | | vex 3436 |
. . . . 5
⊢ 𝑧 ∈ V |
19 | 17, 18 | opelco 5780 |
. . . 4
⊢
(〈𝑦, 𝑧〉 ∈ (𝐴 ∘ ∪
𝑥 ∈ 𝐶 𝐵) ↔ ∃𝑤(𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
20 | 17, 18 | opelco 5780 |
. . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
21 | 20 | rexbii 3181 |
. . . 4
⊢
(∃𝑥 ∈
𝐶 〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑥 ∈ 𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
22 | 16, 19, 21 | 3bitr4i 303 |
. . 3
⊢
(〈𝑦, 𝑧〉 ∈ (𝐴 ∘ ∪
𝑥 ∈ 𝐶 𝐵) ↔ ∃𝑥 ∈ 𝐶 〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵)) |
23 | | eliun 4928 |
. . 3
⊢
(〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) ↔ ∃𝑥 ∈ 𝐶 〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵)) |
24 | 22, 23 | bitr4i 277 |
. 2
⊢
(〈𝑦, 𝑧〉 ∈ (𝐴 ∘ ∪
𝑥 ∈ 𝐶 𝐵) ↔ 〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)) |
25 | 1, 5, 24 | eqrelriiv 5700 |
1
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪
𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) |