Theorem trclubi

Description: The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 2-Jan-2020) (Revised by RP, 28-Apr-2020) (Revised by AV, 26-Mar-2021)

	Ref	Expression
Hypotheses	trclubi.rel	|- Rel R
	trclubi.rex	|- R e. _V
Assertion	trclubi	|- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( dom R X. ran R )

Proof

Step	Hyp	Ref	Expression
1		trclubi.rel	|- Rel R
2		trclubi.rex	|- R e. _V
3		relssdmrn	|- ( Rel R -> R C_ ( dom R X. ran R ) )
4		ssequn1	|- ( R C_ ( dom R X. ran R ) <-> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
5	3 4	sylib	|- ( Rel R -> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
6	1 5	ax-mp	|- ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R )
7		trclublem	|- ( R e. _V -> ( R u. ( dom R X. ran R ) ) e. { s | ( R C_ s /\ ( s o. s ) C_ s ) } )
8	2 7	ax-mp	|- ( R u. ( dom R X. ran R ) ) e. { s | ( R C_ s /\ ( s o. s ) C_ s ) }
9	6 8	eqeltrri	|- ( dom R X. ran R ) e. { s | ( R C_ s /\ ( s o. s ) C_ s ) }
10		intss1	|- ( ( dom R X. ran R ) e. { s | ( R C_ s /\ ( s o. s ) C_ s ) } -> |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( dom R X. ran R ) )
11	9 10	ax-mp	|- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( dom R X. ran R )