Metamath Proof Explorer

Theorem reltrclfv

Description: The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020)

Ref Expression
Assertion reltrclfv 
|- ( ( R e. V /\ Rel R ) -> Rel ( t+ ` R ) )

Proof

Step Hyp Ref Expression
1 trclfvub 
 |-  ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )
2 1 adantr 
 |-  ( ( R e. V /\ Rel R ) -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )
3 simpr 
 |-  ( ( R e. V /\ Rel R ) -> Rel R )
4 relssdmrn 
 |-  ( Rel R -> R C_ ( dom R X. ran R ) )
5 ssequn1 
 |-  ( R C_ ( dom R X. ran R ) <-> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
6 5 biimpi 
 |-  ( R C_ ( dom R X. ran R ) -> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
7 3 4 6 3syl 
 |-  ( ( R e. V /\ Rel R ) -> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
8 2 7 sseqtrd 
 |-  ( ( R e. V /\ Rel R ) -> ( t+ ` R ) C_ ( dom R X. ran R ) )
9 xpss 
 |-  ( dom R X. ran R ) C_ ( _V X. _V )
10 8 9 sstrdi 
 |-  ( ( R e. V /\ Rel R ) -> ( t+ ` R ) C_ ( _V X. _V ) )
11 df-rel 
 |-  ( Rel ( t+ ` R ) <-> ( t+ ` R ) C_ ( _V X. _V ) )
12 10 11 sylibr 
 |-  ( ( R e. V /\ Rel R ) -> Rel ( t+ ` R ) )