Metamath Proof Explorer

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 
|- ( X e. V -> ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = ran 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 rnss 
 |-  ( |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ ( X u. ( dom X X. ran X ) ) -> ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ ran ( X u. ( dom X X. ran X ) ) )
3 1 2 syl 
 |-  ( X e. V -> ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ ran ( X u. ( dom X X. ran X ) ) )
4 rnun 
 |-  ran ( X u. ( dom X X. ran X ) ) = ( ran X u. ran ( dom X X. ran X ) )
5 rnxpss 
 |-  ran ( dom X X. ran X ) C_ ran X
6 ssequn2 
 |-  ( ran ( dom X X. ran X ) C_ ran X <-> ( ran X u. ran ( dom X X. ran X ) ) = ran X )
7 5 6 mpbi 
 |-  ( ran X u. ran ( dom X X. ran X ) ) = ran X
8 4 7 eqtri 
 |-  ran ( X u. ( dom X X. ran X ) ) = ran X
9 3 8 sseqtrdi 
 |-  ( X e. V -> ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } C_ ran X )
10 ssmin 
 |-  X C_ |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) }
11 rnss 
 |-  ( X C_ |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } -> ran X C_ ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } )
12 10 11 mp1i 
 |-  ( X e. V -> ran X C_ ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } )
13 9 12 eqssd 
 |-  ( X e. V -> ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = ran X )