Theorem rntrclfvOAI

Description: The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020)

	Ref	Expression
Assertion	rntrclfvOAI	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) = ran 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		trclfvub	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
2		rnss	⊢ ( ( t+ ‘ 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) → ran ( t+ ‘ 𝑅 ) ⊆ ran ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
3	1 2	syl	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) ⊆ ran ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
4		rnun	⊢ ran ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( ran 𝑅 ∪ ran ( dom 𝑅 × ran 𝑅 ) )
5	4	a1i	⊢ ( 𝑅 ∈ 𝑉 → ran ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( ran 𝑅 ∪ ran ( dom 𝑅 × ran 𝑅 ) ) )
6		rnxpss	⊢ ran ( dom 𝑅 × ran 𝑅 ) ⊆ ran 𝑅
7		ssequn2	⊢ ( ran ( dom 𝑅 × ran 𝑅 ) ⊆ ran 𝑅 ↔ ( ran 𝑅 ∪ ran ( dom 𝑅 × ran 𝑅 ) ) = ran 𝑅 )
8	6 7	mpbi	⊢ ( ran 𝑅 ∪ ran ( dom 𝑅 × ran 𝑅 ) ) = ran 𝑅
9	5 8	eqtrdi	⊢ ( 𝑅 ∈ 𝑉 → ran ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ran 𝑅 )
10	3 9	sseqtrd	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) ⊆ ran 𝑅 )
11		trclfvlb	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
12		rnss	⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) → ran 𝑅 ⊆ ran ( t+ ‘ 𝑅 ) )
13	11 12	syl	⊢ ( 𝑅 ∈ 𝑉 → ran 𝑅 ⊆ ran ( t+ ‘ 𝑅 ) )
14	10 13	eqssd	⊢ ( 𝑅 ∈ 𝑉 → ran ( t+ ‘ 𝑅 ) = ran 𝑅 )