Theorem rntrcl

Description: The range of the transitive closure is equal to the range of its base relation. (Contributed by RP, 1-Nov-2020)

	Ref	Expression
Assertion	rntrcl	⊢ ( 𝑋 ∈ 𝑉 → ran ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = ran 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		trclubg	⊢ ( 𝑋 ∈ 𝑉 → ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) )
2		rnss	⊢ ( ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) → ran ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ran ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) )
3	1 2	syl	⊢ ( 𝑋 ∈ 𝑉 → ran ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ran ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) )
4		rnun	⊢ ran ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) = ( ran 𝑋 ∪ ran ( dom 𝑋 × ran 𝑋 ) )
5		rnxpss	⊢ ran ( dom 𝑋 × ran 𝑋 ) ⊆ ran 𝑋
6		ssequn2	⊢ ( ran ( dom 𝑋 × ran 𝑋 ) ⊆ ran 𝑋 ↔ ( ran 𝑋 ∪ ran ( dom 𝑋 × ran 𝑋 ) ) = ran 𝑋 )
7	5 6	mpbi	⊢ ( ran 𝑋 ∪ ran ( dom 𝑋 × ran 𝑋 ) ) = ran 𝑋
8	4 7	eqtri	⊢ ran ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) = ran 𝑋
9	3 8	sseqtrdi	⊢ ( 𝑋 ∈ 𝑉 → ran ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ran 𝑋 )
10		ssmin	⊢ 𝑋 ⊆ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) }
11		rnss	⊢ ( 𝑋 ⊆ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } → ran 𝑋 ⊆ ran ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
12	10 11	mp1i	⊢ ( 𝑋 ∈ 𝑉 → ran 𝑋 ⊆ ran ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
13	9 12	eqssd	⊢ ( 𝑋 ∈ 𝑉 → ran ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = ran 𝑋 )