Theorem dmtrcl

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

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

Proof

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