Proof of Theorem relcnvtr
Step | Hyp | Ref
| Expression |
1 | | cnvco 4784 |
. . 3
⊢ ◡(𝑅 ∘ 𝑅) = (◡𝑅 ∘ ◡𝑅) |
2 | | cnvss 4772 |
. . 3
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ◡(𝑅 ∘ 𝑅) ⊆ ◡𝑅) |
3 | 1, 2 | eqsstrrid 3185 |
. 2
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅) |
4 | | cnvco 4784 |
. . . 4
⊢ ◡(◡𝑅 ∘ ◡𝑅) = (◡◡𝑅 ∘ ◡◡𝑅) |
5 | | cnvss 4772 |
. . . 4
⊢ ((◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅 → ◡(◡𝑅 ∘ ◡𝑅) ⊆ ◡◡𝑅) |
6 | | sseq1 3161 |
. . . . 5
⊢ (◡(◡𝑅 ∘ ◡𝑅) = (◡◡𝑅 ∘ ◡◡𝑅) → (◡(◡𝑅 ∘ ◡𝑅) ⊆ ◡◡𝑅 ↔ (◡◡𝑅 ∘ ◡◡𝑅) ⊆ ◡◡𝑅)) |
7 | | dfrel2 5049 |
. . . . . . 7
⊢ (Rel
𝑅 ↔ ◡◡𝑅 = 𝑅) |
8 | | coeq1 4756 |
. . . . . . . . . 10
⊢ (◡◡𝑅 = 𝑅 → (◡◡𝑅 ∘ ◡◡𝑅) = (𝑅 ∘ ◡◡𝑅)) |
9 | | coeq2 4757 |
. . . . . . . . . 10
⊢ (◡◡𝑅 = 𝑅 → (𝑅 ∘ ◡◡𝑅) = (𝑅 ∘ 𝑅)) |
10 | 8, 9 | eqtrd 2197 |
. . . . . . . . 9
⊢ (◡◡𝑅 = 𝑅 → (◡◡𝑅 ∘ ◡◡𝑅) = (𝑅 ∘ 𝑅)) |
11 | | id 19 |
. . . . . . . . 9
⊢ (◡◡𝑅 = 𝑅 → ◡◡𝑅 = 𝑅) |
12 | 10, 11 | sseq12d 3169 |
. . . . . . . 8
⊢ (◡◡𝑅 = 𝑅 → ((◡◡𝑅 ∘ ◡◡𝑅) ⊆ ◡◡𝑅 ↔ (𝑅 ∘ 𝑅) ⊆ 𝑅)) |
13 | 12 | biimpd 143 |
. . . . . . 7
⊢ (◡◡𝑅 = 𝑅 → ((◡◡𝑅 ∘ ◡◡𝑅) ⊆ ◡◡𝑅 → (𝑅 ∘ 𝑅) ⊆ 𝑅)) |
14 | 7, 13 | sylbi 120 |
. . . . . 6
⊢ (Rel
𝑅 → ((◡◡𝑅 ∘ ◡◡𝑅) ⊆ ◡◡𝑅 → (𝑅 ∘ 𝑅) ⊆ 𝑅)) |
15 | 14 | com12 30 |
. . . . 5
⊢ ((◡◡𝑅 ∘ ◡◡𝑅) ⊆ ◡◡𝑅 → (Rel 𝑅 → (𝑅 ∘ 𝑅) ⊆ 𝑅)) |
16 | 6, 15 | syl6bi 162 |
. . . 4
⊢ (◡(◡𝑅 ∘ ◡𝑅) = (◡◡𝑅 ∘ ◡◡𝑅) → (◡(◡𝑅 ∘ ◡𝑅) ⊆ ◡◡𝑅 → (Rel 𝑅 → (𝑅 ∘ 𝑅) ⊆ 𝑅))) |
17 | 4, 5, 16 | mpsyl 65 |
. . 3
⊢ ((◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅 → (Rel 𝑅 → (𝑅 ∘ 𝑅) ⊆ 𝑅)) |
18 | 17 | com12 30 |
. 2
⊢ (Rel
𝑅 → ((◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅 → (𝑅 ∘ 𝑅) ⊆ 𝑅)) |
19 | 3, 18 | impbid2 142 |
1
⊢ (Rel
𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅)) |