Proof of Theorem trrelsuperrel2dg
| Step | Hyp | Ref
| Expression |
| 1 | | ssun1 4178 |
. . 3
⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 2 | | trrelsuperrel2dg.s |
. . 3
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 3 | 1, 2 | sseqtrrid 4027 |
. 2
⊢ (𝜑 → 𝑅 ⊆ 𝑆) |
| 4 | | xptrrel 15019 |
. . . . 5
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅) |
| 5 | | ssun2 4179 |
. . . . 5
⊢ (dom
𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 6 | 4, 5 | sstri 3993 |
. . . 4
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
| 7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 8 | 2, 2 | coeq12d 5875 |
. . . 4
⊢ (𝜑 → (𝑆 ∘ 𝑆) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 9 | | coundir 6268 |
. . . . . 6
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ∪ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 10 | | relcnv 6122 |
. . . . . . 7
⊢ Rel ◡◡𝑅 |
| 11 | | cocnvcnv1 6277 |
. . . . . . . . 9
⊢ (◡◡𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 12 | | relssdmrn 6288 |
. . . . . . . . . . 11
⊢ (Rel
◡◡𝑅 → ◡◡𝑅 ⊆ (dom ◡◡𝑅 × ran ◡◡𝑅)) |
| 13 | | dmcnvcnv 5944 |
. . . . . . . . . . . 12
⊢ dom ◡◡𝑅 = dom 𝑅 |
| 14 | | rncnvcnv 5945 |
. . . . . . . . . . . 12
⊢ ran ◡◡𝑅 = ran 𝑅 |
| 15 | 13, 14 | xpeq12i 5713 |
. . . . . . . . . . 11
⊢ (dom
◡◡𝑅 × ran ◡◡𝑅) = (dom 𝑅 × ran 𝑅) |
| 16 | 12, 15 | sseqtrdi 4024 |
. . . . . . . . . 10
⊢ (Rel
◡◡𝑅 → ◡◡𝑅 ⊆ (dom 𝑅 × ran 𝑅)) |
| 17 | | coss1 5866 |
. . . . . . . . . 10
⊢ (◡◡𝑅 ⊆ (dom 𝑅 × ran 𝑅) → (◡◡𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (Rel
◡◡𝑅 → (◡◡𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 19 | 11, 18 | eqsstrrid 4023 |
. . . . . . . 8
⊢ (Rel
◡◡𝑅 → (𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 20 | | ssequn1 4186 |
. . . . . . . 8
⊢ ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ↔ ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ∪ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) = ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 21 | 19, 20 | sylib 218 |
. . . . . . 7
⊢ (Rel
◡◡𝑅 → ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ∪ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) = ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
| 22 | 10, 21 | ax-mp 5 |
. . . . . 6
⊢ ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ∪ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) = ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 23 | 9, 22 | eqtri 2765 |
. . . . 5
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 24 | | coundi 6267 |
. . . . . 6
⊢ ((dom
𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (((dom 𝑅 × ran 𝑅) ∘ 𝑅) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 25 | | cocnvcnv2 6278 |
. . . . . . . . 9
⊢ ((dom
𝑅 × ran 𝑅) ∘ ◡◡𝑅) = ((dom 𝑅 × ran 𝑅) ∘ 𝑅) |
| 26 | | coss2 5867 |
. . . . . . . . . 10
⊢ (◡◡𝑅 ⊆ (dom 𝑅 × ran 𝑅) → ((dom 𝑅 × ran 𝑅) ∘ ◡◡𝑅) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 27 | 16, 26 | syl 17 |
. . . . . . . . 9
⊢ (Rel
◡◡𝑅 → ((dom 𝑅 × ran 𝑅) ∘ ◡◡𝑅) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 28 | 25, 27 | eqsstrrid 4023 |
. . . . . . . 8
⊢ (Rel
◡◡𝑅 → ((dom 𝑅 × ran 𝑅) ∘ 𝑅) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 29 | | ssequn1 4186 |
. . . . . . . 8
⊢ (((dom
𝑅 × ran 𝑅) ∘ 𝑅) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ↔ (((dom 𝑅 × ran 𝑅) ∘ 𝑅) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 30 | 28, 29 | sylib 218 |
. . . . . . 7
⊢ (Rel
◡◡𝑅 → (((dom 𝑅 × ran 𝑅) ∘ 𝑅) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 31 | 10, 30 | ax-mp 5 |
. . . . . 6
⊢ (((dom
𝑅 × ran 𝑅) ∘ 𝑅) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
| 32 | 24, 31 | eqtri 2765 |
. . . . 5
⊢ ((dom
𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
| 33 | 23, 32 | eqtri 2765 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
| 34 | 8, 33 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → (𝑆 ∘ 𝑆) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
| 35 | 7, 34, 2 | 3sstr4d 4039 |
. 2
⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) |
| 36 | 3, 35 | jca 511 |
1
⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) |