Step | Hyp | Ref
| Expression |
1 | | relco 6064 |
. 2
⊢ Rel
(𝐴 ∘ 𝐵) |
2 | | reliun 5776 |
. . 3
⊢ (Rel
∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∀𝑥 ∈ V Rel ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
3 | | relxp 5655 |
. . . 4
⊢ Rel
((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝑥 ∈ V → Rel ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
5 | 2, 4 | mprgbir 3068 |
. 2
⊢ Rel
∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |
6 | | opelco2g 5827 |
. . . 4
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑥(⟨𝑦, 𝑥⟩ ∈ 𝐵 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴))) |
7 | 6 | el2v 3455 |
. . 3
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑥(⟨𝑦, 𝑥⟩ ∈ 𝐵 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)) |
8 | | eliun 4962 |
. . . 4
⊢
(⟨𝑦, 𝑧⟩ ∈ ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥 ∈ V ⟨𝑦, 𝑧⟩ ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
9 | | rexv 3472 |
. . . 4
⊢
(∃𝑥 ∈ V
⟨𝑦, 𝑧⟩ ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥⟨𝑦, 𝑧⟩ ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
10 | | opelxp 5673 |
. . . . . 6
⊢
(⟨𝑦, 𝑧⟩ ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ (𝑦 ∈ (◡𝐵 “ {𝑥}) ∧ 𝑧 ∈ (𝐴 “ {𝑥}))) |
11 | | vex 3451 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
12 | | vex 3451 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
13 | 11, 12 | elimasn 6045 |
. . . . . . . 8
⊢ (𝑦 ∈ (◡𝐵 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ ◡𝐵) |
14 | 11, 12 | opelcnv 5841 |
. . . . . . . 8
⊢
(⟨𝑥, 𝑦⟩ ∈ ◡𝐵 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝐵) |
15 | 13, 14 | bitri 275 |
. . . . . . 7
⊢ (𝑦 ∈ (◡𝐵 “ {𝑥}) ↔ ⟨𝑦, 𝑥⟩ ∈ 𝐵) |
16 | | vex 3451 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
17 | 11, 16 | elimasn 6045 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 “ {𝑥}) ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐴) |
18 | 15, 17 | anbi12i 628 |
. . . . . 6
⊢ ((𝑦 ∈ (◡𝐵 “ {𝑥}) ∧ 𝑧 ∈ (𝐴 “ {𝑥})) ↔ (⟨𝑦, 𝑥⟩ ∈ 𝐵 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)) |
19 | 10, 18 | bitri 275 |
. . . . 5
⊢
(⟨𝑦, 𝑧⟩ ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ (⟨𝑦, 𝑥⟩ ∈ 𝐵 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)) |
20 | 19 | exbii 1851 |
. . . 4
⊢
(∃𝑥⟨𝑦, 𝑧⟩ ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥(⟨𝑦, 𝑥⟩ ∈ 𝐵 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)) |
21 | 8, 9, 20 | 3bitrri 298 |
. . 3
⊢
(∃𝑥(⟨𝑦, 𝑥⟩ ∈ 𝐵 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) ↔ ⟨𝑦, 𝑧⟩ ∈ ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
22 | 7, 21 | bitri 275 |
. 2
⊢
(⟨𝑦, 𝑧⟩ ∈ (𝐴 ∘ 𝐵) ↔ ⟨𝑦, 𝑧⟩ ∈ ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
23 | 1, 5, 22 | eqrelriiv 5750 |
1
⊢ (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |