Proof of Theorem cnvssco
Step | Hyp | Ref
| Expression |
1 | | alcom 2160 |
. 2
⊢
(∀𝑦∀𝑥(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) ↔ ∀𝑥∀𝑦(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
2 | | relcnv 6010 |
. . 3
⊢ Rel ◡𝐴 |
3 | | ssrel 5692 |
. . 3
⊢ (Rel
◡𝐴 → (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑦∀𝑥(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)))) |
4 | 2, 3 | ax-mp 5 |
. 2
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑦∀𝑥(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
5 | | 19.37v 1999 |
. . . 4
⊢
(∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ (𝑥𝐴𝑦 → ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) |
6 | | vex 3435 |
. . . . . . 7
⊢ 𝑦 ∈ V |
7 | | vex 3435 |
. . . . . . 7
⊢ 𝑥 ∈ V |
8 | 6, 7 | brcnv 5789 |
. . . . . 6
⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦) |
9 | | df-br 5080 |
. . . . . 6
⊢ (𝑦◡𝐴𝑥 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝐴) |
10 | 8, 9 | bitr3i 276 |
. . . . 5
⊢ (𝑥𝐴𝑦 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝐴) |
11 | 7, 6 | brco 5777 |
. . . . . 6
⊢ (𝑥(𝐵 ∘ 𝐶)𝑦 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) |
12 | 6, 7 | brcnv 5789 |
. . . . . . 7
⊢ (𝑦◡(𝐵 ∘ 𝐶)𝑥 ↔ 𝑥(𝐵 ∘ 𝐶)𝑦) |
13 | | df-br 5080 |
. . . . . . 7
⊢ (𝑦◡(𝐵 ∘ 𝐶)𝑥 ↔ 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) |
14 | 12, 13 | bitr3i 276 |
. . . . . 6
⊢ (𝑥(𝐵 ∘ 𝐶)𝑦 ↔ 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) |
15 | 11, 14 | bitr3i 276 |
. . . . 5
⊢
(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦) ↔ 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) |
16 | 10, 15 | imbi12i 351 |
. . . 4
⊢ ((𝑥𝐴𝑦 → ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ (〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
17 | 5, 16 | bitri 274 |
. . 3
⊢
(∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ (〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
18 | 17 | 2albii 1827 |
. 2
⊢
(∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ ∀𝑥∀𝑦(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
19 | 1, 4, 18 | 3bitr4i 303 |
1
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) |