Step |
Hyp |
Ref |
Expression |
1 |
|
trclfvub |
⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) |
3 |
|
simpr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → Rel 𝑅 ) |
4 |
|
relssdmrn |
⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ) |
5 |
|
ssequn1 |
⊢ ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ↔ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) ) |
6 |
5
|
biimpi |
⊢ ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) ) |
7 |
3 4 6
|
3syl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) ) |
8 |
2 7
|
sseqtrd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( t+ ‘ 𝑅 ) ⊆ ( dom 𝑅 × ran 𝑅 ) ) |
9 |
|
xpss |
⊢ ( dom 𝑅 × ran 𝑅 ) ⊆ ( V × V ) |
10 |
8 9
|
sstrdi |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( t+ ‘ 𝑅 ) ⊆ ( V × V ) ) |
11 |
|
df-rel |
⊢ ( Rel ( t+ ‘ 𝑅 ) ↔ ( t+ ‘ 𝑅 ) ⊆ ( V × V ) ) |
12 |
10 11
|
sylibr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → Rel ( t+ ‘ 𝑅 ) ) |