Proof of Theorem trrelsuperrel2dg
Step | Hyp | Ref
| Expression |
1 | | ssun1 4063 |
. . 3
⊢ 𝑅 ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
2 | | trrelsuperrel2dg.s |
. . 3
⊢ (𝜑 → 𝑆 = (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
3 | 1, 2 | sseqtrrid 3931 |
. 2
⊢ (𝜑 → 𝑅 ⊆ 𝑆) |
4 | | xptrrel 14430 |
. . . . 5
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (dom 𝑅 × ran 𝑅) |
5 | | ssun2 4064 |
. . . . 5
⊢ (dom
𝑅 × ran 𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
6 | 4, 5 | sstri 3887 |
. . . 4
⊢ ((dom
𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
8 | 2, 2 | coeq12d 5708 |
. . . 4
⊢ (𝜑 → (𝑆 ∘ 𝑆) = ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
9 | | coundir 6082 |
. . . . . 6
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ∪ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
10 | | relcnv 5942 |
. . . . . . 7
⊢ Rel ◡◡𝑅 |
11 | | cocnvcnv1 6091 |
. . . . . . . . 9
⊢ (◡◡𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
12 | | relssdmrn 6102 |
. . . . . . . . . . 11
⊢ (Rel
◡◡𝑅 → ◡◡𝑅 ⊆ (dom ◡◡𝑅 × ran ◡◡𝑅)) |
13 | | dmcnvcnv 5777 |
. . . . . . . . . . . 12
⊢ dom ◡◡𝑅 = dom 𝑅 |
14 | | rncnvcnv 5778 |
. . . . . . . . . . . 12
⊢ ran ◡◡𝑅 = ran 𝑅 |
15 | 13, 14 | xpeq12i 5554 |
. . . . . . . . . . 11
⊢ (dom
◡◡𝑅 × ran ◡◡𝑅) = (dom 𝑅 × ran 𝑅) |
16 | 12, 15 | sseqtrdi 3928 |
. . . . . . . . . 10
⊢ (Rel
◡◡𝑅 → ◡◡𝑅 ⊆ (dom 𝑅 × ran 𝑅)) |
17 | | coss1 5699 |
. . . . . . . . . 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 3927 |
. . . . . . . 8
⊢ (Rel
◡◡𝑅 → (𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
20 | | ssequn1 4071 |
. . . . . . . 8
⊢ ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ↔ ((𝑅 ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) ∪ ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) = ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))) |
21 | 19, 20 | sylib 221 |
. . . . . . 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 2761 |
. . . . 5
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
24 | | coundi 6081 |
. . . . . 6
⊢ ((dom
𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = (((dom 𝑅 × ran 𝑅) ∘ 𝑅) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
25 | | cocnvcnv2 6092 |
. . . . . . . . 9
⊢ ((dom
𝑅 × ran 𝑅) ∘ ◡◡𝑅) = ((dom 𝑅 × ran 𝑅) ∘ 𝑅) |
26 | | coss2 5700 |
. . . . . . . . . 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 3927 |
. . . . . . . 8
⊢ (Rel
◡◡𝑅 → ((dom 𝑅 × ran 𝑅) ∘ 𝑅) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
29 | | ssequn1 4071 |
. . . . . . . 8
⊢ (((dom
𝑅 × ran 𝑅) ∘ 𝑅) ⊆ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) ↔ (((dom 𝑅 × ran 𝑅) ∘ 𝑅) ∪ ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
30 | 28, 29 | sylib 221 |
. . . . . . 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 2761 |
. . . . 5
⊢ ((dom
𝑅 × ran 𝑅) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
33 | 23, 32 | eqtri 2761 |
. . . 4
⊢ ((𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅)) |
34 | 8, 33 | eqtrdi 2789 |
. . 3
⊢ (𝜑 → (𝑆 ∘ 𝑆) = ((dom 𝑅 × ran 𝑅) ∘ (dom 𝑅 × ran 𝑅))) |
35 | 7, 34, 2 | 3sstr4d 3925 |
. 2
⊢ (𝜑 → (𝑆 ∘ 𝑆) ⊆ 𝑆) |
36 | 3, 35 | jca 515 |
1
⊢ (𝜑 → (𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆)) |