Metamath Proof Explorer

Theorem trclubg

Description: The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure (as a relation). (Contributed by RP, 17-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		trclublem	\|- ( R e. V -> ( R u. ( dom R X. ran R ) ) e. { r \| ( R C_ r /\ ( r o. r ) C_ r ) } )
2		intss1	\|- ( ( R u. ( dom R X. ran R ) ) e. { r \| ( R C_ r /\ ( r o. r ) C_ r ) } -> \|^\| { r \| ( R C_ r /\ ( r o. r ) C_ r ) } C_ ( R u. ( dom R X. ran R ) ) )
3	1 2	syl	\|- ( R e. V -> \|^\| { r \| ( R C_ r /\ ( r o. r ) C_ r ) } C_ ( R u. ( dom R X. ran R ) ) )

Step

Hyp

Ref

Expression

trclublem

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

intss1

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

1 2

syl

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