Theorem trclub

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

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

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	|- ( Rel R -> R C_ ( dom R X. ran R ) )
2		ssequn1	|- ( R C_ ( dom R X. ran R ) <-> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
3	1 2	sylib	|- ( Rel R -> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
4		trclublem	|- ( R e. V -> ( R u. ( dom R X. ran R ) ) e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
5		eleq1	|- ( ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) -> ( ( R u. ( dom R X. ran R ) ) e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } <-> ( dom R X. ran R ) e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } ) )
6	5	biimpa	|- ( ( ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) /\ ( R u. ( dom R X. ran R ) ) e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } ) -> ( dom R X. ran R ) e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
7	3 4 6	syl2anr	|- ( ( R e. V /\ Rel R ) -> ( dom R X. ran R ) e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
8		intss1	|- ( ( 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_ ( dom R X. ran R ) )
9	7 8	syl	|- ( ( R e. V /\ Rel R ) -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ ( dom R X. ran R ) )