Theorem dmtrclfv

Description: The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020)

	Ref	Expression
Assertion	dmtrclfv	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ 𝑅 ) = dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		trclfvub	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
2		dmss	⊢ ( ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) → dom ( t+ ‘ 𝑅 ) ⊆ dom ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
3	1 2	syl	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ 𝑅 ) ⊆ dom ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
4		dmun	⊢ dom ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 ∪ dom ( dom 𝑅 × ran 𝑅 ) )
5		dm0rn0	⊢ ( dom 𝑅 = ∅ ↔ ran 𝑅 = ∅ )
6		xpeq1	⊢ ( dom 𝑅 = ∅ → ( dom 𝑅 × ran 𝑅 ) = ( ∅ × ran 𝑅 ) )
7		0xp	⊢ ( ∅ × ran 𝑅 ) = ∅
8	6 7	eqtrdi	⊢ ( dom 𝑅 = ∅ → ( dom 𝑅 × ran 𝑅 ) = ∅ )
9	8	dmeqd	⊢ ( dom 𝑅 = ∅ → dom ( dom 𝑅 × ran 𝑅 ) = dom ∅ )
10		dm0	⊢ dom ∅ = ∅
11	10	a1i	⊢ ( dom 𝑅 = ∅ → dom ∅ = ∅ )
12		eqcom	⊢ ( dom 𝑅 = ∅ ↔ ∅ = dom 𝑅 )
13	12	biimpi	⊢ ( dom 𝑅 = ∅ → ∅ = dom 𝑅 )
14	9 11 13	3eqtrd	⊢ ( dom 𝑅 = ∅ → dom ( dom 𝑅 × ran 𝑅 ) = dom 𝑅 )
15	5 14	sylbir	⊢ ( ran 𝑅 = ∅ → dom ( dom 𝑅 × ran 𝑅 ) = dom 𝑅 )
16		dmxp	⊢ ( ran 𝑅 ≠ ∅ → dom ( dom 𝑅 × ran 𝑅 ) = dom 𝑅 )
17	15 16	pm2.61ine	⊢ dom ( dom 𝑅 × ran 𝑅 ) = dom 𝑅
18	17	uneq2i	⊢ ( dom 𝑅 ∪ dom ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 ∪ dom 𝑅 )
19		unidm	⊢ ( dom 𝑅 ∪ dom 𝑅 ) = dom 𝑅
20	4 18 19	3eqtri	⊢ dom ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = dom 𝑅
21	3 20	sseqtrdi	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ 𝑅 ) ⊆ dom 𝑅 )
22		trclfvlb	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
23		dmss	⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) → dom 𝑅 ⊆ dom ( t+ ‘ 𝑅 ) )
24	22 23	syl	⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ⊆ dom ( t+ ‘ 𝑅 ) )
25	21 24	eqssd	⊢ ( 𝑅 ∈ 𝑉 → dom ( t+ ‘ 𝑅 ) = dom 𝑅 )