Proof of Theorem cnvssco
| Step | Hyp | Ref
| Expression |
| 1 | | alcom 2159 |
. 2
⊢
(∀𝑦∀𝑥(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) ↔ ∀𝑥∀𝑦(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
| 2 | | relcnv 6122 |
. . 3
⊢ Rel ◡𝐴 |
| 3 | | ssrel 5792 |
. . 3
⊢ (Rel
◡𝐴 → (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑦∀𝑥(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)))) |
| 4 | 2, 3 | ax-mp 5 |
. 2
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑦∀𝑥(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
| 5 | | 19.37v 1991 |
. . . 4
⊢
(∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ (𝑥𝐴𝑦 → ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) |
| 6 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 7 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 8 | 6, 7 | brcnv 5893 |
. . . . . 6
⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦) |
| 9 | | df-br 5144 |
. . . . . 6
⊢ (𝑦◡𝐴𝑥 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝐴) |
| 10 | 8, 9 | bitr3i 277 |
. . . . 5
⊢ (𝑥𝐴𝑦 ↔ 〈𝑦, 𝑥〉 ∈ ◡𝐴) |
| 11 | 7, 6 | brco 5881 |
. . . . . 6
⊢ (𝑥(𝐵 ∘ 𝐶)𝑦 ↔ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) |
| 12 | 6, 7 | brcnv 5893 |
. . . . . . 7
⊢ (𝑦◡(𝐵 ∘ 𝐶)𝑥 ↔ 𝑥(𝐵 ∘ 𝐶)𝑦) |
| 13 | | df-br 5144 |
. . . . . . 7
⊢ (𝑦◡(𝐵 ∘ 𝐶)𝑥 ↔ 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) |
| 14 | 12, 13 | bitr3i 277 |
. . . . . 6
⊢ (𝑥(𝐵 ∘ 𝐶)𝑦 ↔ 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) |
| 15 | 11, 14 | bitr3i 277 |
. . . . 5
⊢
(∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦) ↔ 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶)) |
| 16 | 10, 15 | imbi12i 350 |
. . . 4
⊢ ((𝑥𝐴𝑦 → ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ (〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
| 17 | 5, 16 | bitri 275 |
. . 3
⊢
(∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ (〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
| 18 | 17 | 2albii 1820 |
. 2
⊢
(∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)) ↔ ∀𝑥∀𝑦(〈𝑦, 𝑥〉 ∈ ◡𝐴 → 〈𝑦, 𝑥〉 ∈ ◡(𝐵 ∘ 𝐶))) |
| 19 | 1, 4, 18 | 3bitr4i 303 |
1
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) |