Metamath Proof Explorer

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 
|- ( X e. V -> dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = dom X )

Proof

Step Hyp Ref Expression
1 trclubg 
 |-  ( X e. V -> |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ ( X u. ( dom X X. ran X ) ) )
2 dmss 
 |-  ( |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ ( X u. ( dom X X. ran X ) ) -> dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ dom ( X u. ( dom X X. ran X ) ) )
3 1 2 syl 
 |-  ( X e. V -> dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ dom ( X u. ( dom X X. ran X ) ) )
4 dmun 
 |-  dom ( X u. ( dom X X. ran X ) ) = ( dom X u. dom ( dom X X. ran X ) )
5 dmxpss 
 |-  dom ( dom X X. ran X ) C_ dom X
6 ssequn2 
 |-  ( dom ( dom X X. ran X ) C_ dom X <-> ( dom X u. dom ( dom X X. ran X ) ) = dom X )
7 5 6 mpbi 
 |-  ( dom X u. dom ( dom X X. ran X ) ) = dom X
8 4 7 eqtri 
 |-  dom ( X u. ( dom X X. ran X ) ) = dom X
9 3 8 sseqtrdi 
 |-  ( X e. V -> dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ dom X )
10 ssmin 
 |-  X C_ |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) }
11 dmss 
 |-  ( X C_ |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } -> dom X C_ dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } )
12 10 11 mp1i 
 |-  ( X e. V -> dom X C_ dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } )
13 9 12 eqssd 
 |-  ( X e. V -> dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = dom X )