Step | Hyp | Ref
| Expression |
1 | | relco 6061 |
. 2
⊢ Rel
(𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) |
2 | | reliun 5773 |
. . 3
⊢ (Rel
∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) ↔ ∀𝑥 ∈ 𝐶 Rel (𝐴 ∘ 𝐵)) |
3 | | relco 6061 |
. . . 4
⊢ Rel
(𝐴 ∘ 𝐵) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝑥 ∈ 𝐶 → Rel (𝐴 ∘ 𝐵)) |
5 | 2, 4 | mprgbir 3068 |
. 2
⊢ Rel
∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) |
6 | | eliun 4959 |
. . . . . . . . 9
⊢
(⟨𝑦, 𝑤⟩ ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ↔ ∃𝑥 ∈ 𝐶 ⟨𝑦, 𝑤⟩ ∈ 𝐵) |
7 | | df-br 5107 |
. . . . . . . . 9
⊢ (𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ↔ ⟨𝑦, 𝑤⟩ ∈ ∪ 𝑥 ∈ 𝐶 𝐵) |
8 | | df-br 5107 |
. . . . . . . . . 10
⊢ (𝑦𝐵𝑤 ↔ ⟨𝑦, 𝑤⟩ ∈ 𝐵) |
9 | 8 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐶 𝑦𝐵𝑤 ↔ ∃𝑥 ∈ 𝐶 ⟨𝑦, 𝑤⟩ ∈ 𝐵) |
10 | 6, 7, 9 | 3bitr4i 303 |
. . . . . . . 8
⊢ (𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ↔ ∃𝑥 ∈ 𝐶 𝑦𝐵𝑤) |
11 | 10 | anbi1i 625 |
. . . . . . 7
⊢ ((𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ (∃𝑥 ∈ 𝐶 𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
12 | | r19.41v 3182 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ (∃𝑥 ∈ 𝐶 𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
13 | 11, 12 | bitr4i 278 |
. . . . . 6
⊢ ((𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
14 | 13 | exbii 1851 |
. . . . 5
⊢
(∃𝑤(𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑤∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
15 | | rexcom4 3270 |
. . . . 5
⊢
(∃𝑥 ∈
𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑤∃𝑥 ∈ 𝐶 (𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
16 | 14, 15 | bitr4i 278 |
. . . 4
⊢
(∃𝑤(𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧) ↔ ∃𝑥 ∈ 𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
17 | | vex 3448 |
. . . . 5
⊢ 𝑦 ∈ V |
18 | | vex 3448 |
. . . . 5
⊢ 𝑧 ∈ V |
19 | 17, 18 | opelco 5828 |
. . . 4
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ ∪
𝑥 ∈ 𝐶 𝐵) ↔ ∃𝑤(𝑦∪ 𝑥 ∈ 𝐶 𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
20 | 17, 18 | opelco 5828 |
. . . . 5
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
21 | 20 | rexbii 3094 |
. . . 4
⊢
(∃𝑥 ∈
𝐶 ⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑥 ∈ 𝐶 ∃𝑤(𝑦𝐵𝑤 ∧ 𝑤𝐴𝑧)) |
22 | 16, 19, 21 | 3bitr4i 303 |
. . 3
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ ∪
𝑥 ∈ 𝐶 𝐵) ↔ ∃𝑥 ∈ 𝐶 ⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ 𝐵)) |
23 | | eliun 4959 |
. . 3
⊢
(⟨𝑦, 𝑧⟩ ∈ ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) ↔ ∃𝑥 ∈ 𝐶 ⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ 𝐵)) |
24 | 22, 23 | bitr4i 278 |
. 2
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ ∪
𝑥 ∈ 𝐶 𝐵) ↔ ⟨𝑦, 𝑧⟩ ∈ ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)) |
25 | 1, 5, 24 | eqrelriiv 5747 |
1
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪
𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) |