Step | Hyp | Ref
| Expression |
1 | | relco 5107 |
. 2
⊢ Rel
(𝐴 ∘ 𝐵) |
2 | | reliun 4730 |
. . 3
⊢ (Rel
∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∀𝑥 ∈ V Rel ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
3 | | relxp 4718 |
. . . 4
⊢ Rel
((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |
4 | 3 | a1i 9 |
. . 3
⊢ (𝑥 ∈ V → Rel ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
5 | 2, 4 | mprgbir 2528 |
. 2
⊢ Rel
∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |
6 | | vex 2733 |
. . . 4
⊢ 𝑦 ∈ V |
7 | | vex 2733 |
. . . 4
⊢ 𝑧 ∈ V |
8 | | opelco2g 4777 |
. . . 4
⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑥(〈𝑦, 𝑥〉 ∈ 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴))) |
9 | 6, 7, 8 | mp2an 424 |
. . 3
⊢
(〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑥(〈𝑦, 𝑥〉 ∈ 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴)) |
10 | | eliun 3875 |
. . . 4
⊢
(〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥 ∈ V 〈𝑦, 𝑧〉 ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
11 | | rexv 2748 |
. . . 4
⊢
(∃𝑥 ∈ V
〈𝑦, 𝑧〉 ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥〈𝑦, 𝑧〉 ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
12 | | opelxp 4639 |
. . . . . 6
⊢
(〈𝑦, 𝑧〉 ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ (𝑦 ∈ (◡𝐵 “ {𝑥}) ∧ 𝑧 ∈ (𝐴 “ {𝑥}))) |
13 | | vex 2733 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
14 | 13, 6 | elimasn 4976 |
. . . . . . . 8
⊢ (𝑦 ∈ (◡𝐵 “ {𝑥}) ↔ 〈𝑥, 𝑦〉 ∈ ◡𝐵) |
15 | 13, 6 | opelcnv 4791 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ◡𝐵 ↔ 〈𝑦, 𝑥〉 ∈ 𝐵) |
16 | 14, 15 | bitri 183 |
. . . . . . 7
⊢ (𝑦 ∈ (◡𝐵 “ {𝑥}) ↔ 〈𝑦, 𝑥〉 ∈ 𝐵) |
17 | 13, 7 | elimasn 4976 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 “ {𝑥}) ↔ 〈𝑥, 𝑧〉 ∈ 𝐴) |
18 | 16, 17 | anbi12i 457 |
. . . . . 6
⊢ ((𝑦 ∈ (◡𝐵 “ {𝑥}) ∧ 𝑧 ∈ (𝐴 “ {𝑥})) ↔ (〈𝑦, 𝑥〉 ∈ 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴)) |
19 | 12, 18 | bitri 183 |
. . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ (〈𝑦, 𝑥〉 ∈ 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴)) |
20 | 19 | exbii 1598 |
. . . 4
⊢
(∃𝑥〈𝑦, 𝑧〉 ∈ ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥(〈𝑦, 𝑥〉 ∈ 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴)) |
21 | 10, 11, 20 | 3bitrri 206 |
. . 3
⊢
(∃𝑥(〈𝑦, 𝑥〉 ∈ 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐴) ↔ 〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
22 | 9, 21 | bitri 183 |
. 2
⊢
(〈𝑦, 𝑧〉 ∈ (𝐴 ∘ 𝐵) ↔ 〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
23 | 1, 5, 22 | eqrelriiv 4703 |
1
⊢ (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |