Step | Hyp | Ref
| Expression |
1 | | dfrel6 37302 |
. . . . . . 7
⊢ (Rel
𝑅 ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅) |
2 | 1 | biimpi 215 |
. . . . . 6
⊢ (Rel
𝑅 → (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = 𝑅) |
3 | 2 | dmeqd 5905 |
. . . . 5
⊢ (Rel
𝑅 → dom (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = dom 𝑅) |
4 | 2 | rneqd 5937 |
. . . . 5
⊢ (Rel
𝑅 → ran (𝑅 ∩ (dom 𝑅 × ran 𝑅)) = ran 𝑅) |
5 | 3, 4 | xpeq12d 5707 |
. . . 4
⊢ (Rel
𝑅 → (dom (𝑅 ∩ (dom 𝑅 × ran 𝑅)) × ran (𝑅 ∩ (dom 𝑅 × ran 𝑅))) = (dom 𝑅 × ran 𝑅)) |
6 | 5 | ineq2d 4212 |
. . 3
⊢ (Rel
𝑅 → (𝑆 ∩ (dom (𝑅 ∩ (dom 𝑅 × ran 𝑅)) × ran (𝑅 ∩ (dom 𝑅 × ran 𝑅)))) = (𝑆 ∩ (dom 𝑅 × ran 𝑅))) |
7 | 6 | sseq2d 4014 |
. 2
⊢ (Rel
𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom (𝑅 ∩ (dom 𝑅 × ran 𝑅)) × ran (𝑅 ∩ (dom 𝑅 × ran 𝑅)))) ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)))) |
8 | | relxp 5694 |
. . . 4
⊢ Rel (dom
𝑅 × ran 𝑅) |
9 | | relin2 5813 |
. . . 4
⊢ (Rel (dom
𝑅 × ran 𝑅) → Rel (𝑅 ∩ (dom 𝑅 × ran 𝑅))) |
10 | | relssinxpdmrn 37304 |
. . . 4
⊢ (Rel
(𝑅 ∩ (dom 𝑅 × ran 𝑅)) → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom (𝑅 ∩ (dom 𝑅 × ran 𝑅)) × ran (𝑅 ∩ (dom 𝑅 × ran 𝑅)))) ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑆)) |
11 | 8, 9, 10 | mp2b 10 |
. . 3
⊢ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom (𝑅 ∩ (dom 𝑅 × ran 𝑅)) × ran (𝑅 ∩ (dom 𝑅 × ran 𝑅)))) ↔ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑆) |
12 | 2 | sseq1d 4013 |
. . 3
⊢ (Rel
𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑆 ↔ 𝑅 ⊆ 𝑆)) |
13 | 11, 12 | bitrid 282 |
. 2
⊢ (Rel
𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom (𝑅 ∩ (dom 𝑅 × ran 𝑅)) × ran (𝑅 ∩ (dom 𝑅 × ran 𝑅)))) ↔ 𝑅 ⊆ 𝑆)) |
14 | 7, 13 | bitr3d 280 |
1
⊢ (Rel
𝑅 → ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑆 ∩ (dom 𝑅 × ran 𝑅)) ↔ 𝑅 ⊆ 𝑆)) |