Proof of Theorem relresfld
Step | Hyp | Ref
| Expression |
1 | | relfld 6178 |
. . . 4
⊢ (Rel
𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) |
2 | 1 | reseq2d 5891 |
. . 3
⊢ (Rel
𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) =
(𝑅 ↾ (dom 𝑅 ∪ ran 𝑅))) |
3 | | resundi 5905 |
. . 3
⊢ (𝑅 ↾ (dom 𝑅 ∪ ran 𝑅)) = ((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅)) |
4 | | eqtr 2761 |
. . . 4
⊢ (((𝑅 ↾ ∪ ∪ 𝑅) = (𝑅 ↾ (dom 𝑅 ∪ ran 𝑅)) ∧ (𝑅 ↾ (dom 𝑅 ∪ ran 𝑅)) = ((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅))) → (𝑅 ↾ ∪ ∪ 𝑅) =
((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅))) |
5 | | resss 5916 |
. . . . 5
⊢ (𝑅 ↾ ran 𝑅) ⊆ 𝑅 |
6 | | resdm 5936 |
. . . . 5
⊢ (Rel
𝑅 → (𝑅 ↾ dom 𝑅) = 𝑅) |
7 | | ssequn2 4117 |
. . . . . 6
⊢ ((𝑅 ↾ ran 𝑅) ⊆ 𝑅 ↔ (𝑅 ∪ (𝑅 ↾ ran 𝑅)) = 𝑅) |
8 | | uneq1 4090 |
. . . . . . . . 9
⊢ ((𝑅 ↾ dom 𝑅) = 𝑅 → ((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅)) = (𝑅 ∪ (𝑅 ↾ ran 𝑅))) |
9 | 8 | eqeq2d 2749 |
. . . . . . . 8
⊢ ((𝑅 ↾ dom 𝑅) = 𝑅 → ((𝑅 ↾ ∪ ∪ 𝑅) =
((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅)) ↔ (𝑅 ↾ ∪ ∪ 𝑅) =
(𝑅 ∪ (𝑅 ↾ ran 𝑅)))) |
10 | | eqtr 2761 |
. . . . . . . . 9
⊢ (((𝑅 ↾ ∪ ∪ 𝑅) = (𝑅 ∪ (𝑅 ↾ ran 𝑅)) ∧ (𝑅 ∪ (𝑅 ↾ ran 𝑅)) = 𝑅) → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅) |
11 | 10 | ex 413 |
. . . . . . . 8
⊢ ((𝑅 ↾ ∪ ∪ 𝑅) = (𝑅 ∪ (𝑅 ↾ ran 𝑅)) → ((𝑅 ∪ (𝑅 ↾ ran 𝑅)) = 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅)) |
12 | 9, 11 | syl6bi 252 |
. . . . . . 7
⊢ ((𝑅 ↾ dom 𝑅) = 𝑅 → ((𝑅 ↾ ∪ ∪ 𝑅) =
((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅)) → ((𝑅 ∪ (𝑅 ↾ ran 𝑅)) = 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅))) |
13 | 12 | com3r 87 |
. . . . . 6
⊢ ((𝑅 ∪ (𝑅 ↾ ran 𝑅)) = 𝑅 → ((𝑅 ↾ dom 𝑅) = 𝑅 → ((𝑅 ↾ ∪ ∪ 𝑅) =
((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅)) → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅))) |
14 | 7, 13 | sylbi 216 |
. . . . 5
⊢ ((𝑅 ↾ ran 𝑅) ⊆ 𝑅 → ((𝑅 ↾ dom 𝑅) = 𝑅 → ((𝑅 ↾ ∪ ∪ 𝑅) =
((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅)) → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅))) |
15 | 5, 6, 14 | mpsyl 68 |
. . . 4
⊢ (Rel
𝑅 → ((𝑅 ↾ ∪ ∪ 𝑅) = ((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅)) → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅)) |
16 | 4, 15 | syl5com 31 |
. . 3
⊢ (((𝑅 ↾ ∪ ∪ 𝑅) = (𝑅 ↾ (dom 𝑅 ∪ ran 𝑅)) ∧ (𝑅 ↾ (dom 𝑅 ∪ ran 𝑅)) = ((𝑅 ↾ dom 𝑅) ∪ (𝑅 ↾ ran 𝑅))) → (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅)) |
17 | 2, 3, 16 | sylancl 586 |
. 2
⊢ (Rel
𝑅 → (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅)) |
18 | 17 | pm2.43i 52 |
1
⊢ (Rel
𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) =
𝑅) |