Metamath Proof Explorer

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 
|- ( R e. V -> ran ( t+ ` R ) = ran R )

Proof

Step Hyp Ref Expression
1 trclfvub 
 |-  ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )
2 rnss 
 |-  ( ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) -> ran ( t+ ` R ) C_ ran ( R u. ( dom R X. ran R ) ) )
3 1 2 syl 
 |-  ( R e. V -> ran ( t+ ` R ) C_ ran ( R u. ( dom R X. ran R ) ) )
4 rnun 
 |-  ran ( R u. ( dom R X. ran R ) ) = ( ran R u. ran ( dom R X. ran R ) )
5 4 a1i 
 |-  ( R e. V -> ran ( R u. ( dom R X. ran R ) ) = ( ran R u. ran ( dom R X. ran R ) ) )
6 rnxpss 
 |-  ran ( dom R X. ran R ) C_ ran R
7 ssequn2 
 |-  ( ran ( dom R X. ran R ) C_ ran R <-> ( ran R u. ran ( dom R X. ran R ) ) = ran R )
8 6 7 mpbi 
 |-  ( ran R u. ran ( dom R X. ran R ) ) = ran R
9 5 8 eqtrdi 
 |-  ( R e. V -> ran ( R u. ( dom R X. ran R ) ) = ran R )
10 3 9 sseqtrd 
 |-  ( R e. V -> ran ( t+ ` R ) C_ ran R )
11 trclfvlb 
 |-  ( R e. V -> R C_ ( t+ ` R ) )
12 rnss 
 |-  ( R C_ ( t+ ` R ) -> ran R C_ ran ( t+ ` R ) )
13 11 12 syl 
 |-  ( R e. V -> ran R C_ ran ( t+ ` R ) )
14 10 13 eqssd 
 |-  ( R e. V -> ran ( t+ ` R ) = ran R )