Proof of Theorem dmtrclfv
| Step | Hyp | Ref
| Expression |
| 1 | | trclfvub 15046 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 2 | | dmss 5913 |
. . . 4
⊢
((t+‘𝑅)
⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) → dom (t+‘𝑅) ⊆ dom (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) ⊆ dom (𝑅 ∪ (dom 𝑅 × ran 𝑅))) |
| 4 | | dmun 5921 |
. . . 4
⊢ dom
(𝑅 ∪ (dom 𝑅 × ran 𝑅)) = (dom 𝑅 ∪ dom (dom 𝑅 × ran 𝑅)) |
| 5 | | dm0rn0 5935 |
. . . . . . 7
⊢ (dom
𝑅 = ∅ ↔ ran
𝑅 =
∅) |
| 6 | | xpeq1 5699 |
. . . . . . . . . 10
⊢ (dom
𝑅 = ∅ → (dom
𝑅 × ran 𝑅) = (∅ × ran 𝑅)) |
| 7 | | 0xp 5784 |
. . . . . . . . . 10
⊢ (∅
× ran 𝑅) =
∅ |
| 8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (dom
𝑅 = ∅ → (dom
𝑅 × ran 𝑅) = ∅) |
| 9 | 8 | dmeqd 5916 |
. . . . . . . 8
⊢ (dom
𝑅 = ∅ → dom (dom
𝑅 × ran 𝑅) = dom
∅) |
| 10 | | dm0 5931 |
. . . . . . . . 9
⊢ dom
∅ = ∅ |
| 11 | 10 | a1i 11 |
. . . . . . . 8
⊢ (dom
𝑅 = ∅ → dom
∅ = ∅) |
| 12 | | eqcom 2744 |
. . . . . . . . 9
⊢ (dom
𝑅 = ∅ ↔ ∅
= dom 𝑅) |
| 13 | 12 | biimpi 216 |
. . . . . . . 8
⊢ (dom
𝑅 = ∅ → ∅
= dom 𝑅) |
| 14 | 9, 11, 13 | 3eqtrd 2781 |
. . . . . . 7
⊢ (dom
𝑅 = ∅ → dom (dom
𝑅 × ran 𝑅) = dom 𝑅) |
| 15 | 5, 14 | sylbir 235 |
. . . . . 6
⊢ (ran
𝑅 = ∅ → dom (dom
𝑅 × ran 𝑅) = dom 𝑅) |
| 16 | | dmxp 5939 |
. . . . . 6
⊢ (ran
𝑅 ≠ ∅ → dom
(dom 𝑅 × ran 𝑅) = dom 𝑅) |
| 17 | 15, 16 | pm2.61ine 3025 |
. . . . 5
⊢ dom (dom
𝑅 × ran 𝑅) = dom 𝑅 |
| 18 | 17 | uneq2i 4165 |
. . . 4
⊢ (dom
𝑅 ∪ dom (dom 𝑅 × ran 𝑅)) = (dom 𝑅 ∪ dom 𝑅) |
| 19 | | unidm 4157 |
. . . 4
⊢ (dom
𝑅 ∪ dom 𝑅) = dom 𝑅 |
| 20 | 4, 18, 19 | 3eqtri 2769 |
. . 3
⊢ dom
(𝑅 ∪ (dom 𝑅 × ran 𝑅)) = dom 𝑅 |
| 21 | 3, 20 | sseqtrdi 4024 |
. 2
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) ⊆ dom 𝑅) |
| 22 | | trclfvlb 15047 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅)) |
| 23 | | dmss 5913 |
. . 3
⊢ (𝑅 ⊆ (t+‘𝑅) → dom 𝑅 ⊆ dom (t+‘𝑅)) |
| 24 | 22, 23 | syl 17 |
. 2
⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ⊆ dom (t+‘𝑅)) |
| 25 | 21, 24 | eqssd 4001 |
1
⊢ (𝑅 ∈ 𝑉 → dom (t+‘𝑅) = dom 𝑅) |