Metamath Proof Explorer

Theorem trclfvub

Description: The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020)

		Ref	Expression
	Assertion	trclfvub	\|- ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )

Step	Hyp	Ref	Expression
1		trclfv	\|- ( R e. V -> ( t+ ` R ) = \|^\| { r \| ( R C_ r /\ ( r o. r ) C_ r ) } )
2		trclubg	\|- ( R e. V -> \|^\| { r \| ( R C_ r /\ ( r o. r ) C_ r ) } C_ ( R u. ( dom R X. ran R ) ) )
3	1 2	eqsstrd	\|- ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )

Step

Hyp

Ref

Expression

 |-  ( R e. V -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )

 |-  ( R e. V -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ ( R u. ( dom R X. ran R ) ) )

1 2

 |-  ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )