Proof of Theorem dmtrclfv
Step | Hyp | Ref
| Expression |
1 | | trclfvub 14358 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
2 | | dmss 5735 |
. . . 4
⊢
((t+‘𝑅)
⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → dom (t+‘𝑅) ⊆ dom (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) ⊆ dom (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
4 | | dmun 5743 |
. . . 4
⊢ dom
(𝑅 ∪ (dom 𝑅 × ran 𝑅)) = (dom 𝑅 ∪ dom (dom 𝑅 × ran 𝑅)) |
5 | | dm0rn0 5759 |
. . . . . . 7
⊢ (dom
𝑅 = ∅ ↔ ran
𝑅 =
∅) |
6 | | xpeq1 5533 |
. . . . . . . . . 10
⊢ (dom
𝑅 = ∅ → (dom
𝑅 × ran 𝑅) = (∅ × ran 𝑅)) |
7 | | 0xp 5613 |
. . . . . . . . . 10
⊢ (∅
× ran 𝑅) =
∅ |
8 | 6, 7 | eqtrdi 2849 |
. . . . . . . . 9
⊢ (dom
𝑅 = ∅ → (dom
𝑅 × ran 𝑅) = ∅) |
9 | 8 | dmeqd 5738 |
. . . . . . . 8
⊢ (dom
𝑅 = ∅ → dom (dom
𝑅 × ran 𝑅) = dom
∅) |
10 | | dm0 5754 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
11 | 10 | a1i 11 |
. . . . . . . 8
⊢ (dom
𝑅 = ∅ → dom
∅ = ∅) |
12 | | eqcom 2805 |
. . . . . . . . 9
⊢ (dom
𝑅 = ∅ ↔ ∅
= dom 𝑅) |
13 | 12 | biimpi 219 |
. . . . . . . 8
⊢ (dom
𝑅 = ∅ → ∅
= dom 𝑅) |
14 | 9, 11, 13 | 3eqtrd 2837 |
. . . . . . 7
⊢ (dom
𝑅 = ∅ → dom (dom
𝑅 × ran 𝑅) = dom 𝑅) |
15 | 5, 14 | sylbir 238 |
. . . . . 6
⊢ (ran
𝑅 = ∅ → dom (dom
𝑅 × ran 𝑅) = dom 𝑅) |
16 | | dmxp 5763 |
. . . . . 6
⊢ (ran
𝑅 ≠ ∅ → dom
(dom 𝑅 × ran 𝑅) = dom 𝑅) |
17 | 15, 16 | pm2.61ine 3070 |
. . . . 5
⊢ dom (dom
𝑅 × ran 𝑅) = dom 𝑅 |
18 | 17 | uneq2i 4087 |
. . . 4
⊢ (dom
𝑅 ∪ dom (dom 𝑅 × ran 𝑅)) = (dom 𝑅 ∪ dom 𝑅) |
19 | | unidm 4079 |
. . . 4
⊢ (dom
𝑅 ∪ dom 𝑅) = dom 𝑅 |
20 | 4, 18, 19 | 3eqtri 2825 |
. . 3
⊢ dom
(𝑅 ∪ (dom 𝑅 × ran 𝑅)) = dom 𝑅 |
21 | 3, 20 | sseqtrdi 3965 |
. 2
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) ⊆ dom 𝑅) |
22 | | trclfvlb 14359 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅)) |
23 | | dmss 5735 |
. . 3
⊢ (𝑅 ⊆ (t+‘𝑅) → dom 𝑅 ⊆ dom (t+‘𝑅)) |
24 | 22, 23 | syl 17 |
. 2
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ⊆ dom (t+‘𝑅)) |
25 | 21, 24 | eqssd 3932 |
1
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅) |