Theorem trclubgi

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

	Ref	Expression
Hypothesis	trclubgi.rex	|- R e. _V
Assertion	trclubgi	|- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( R u. ( dom R X. ran R ) )

Proof

Step	Hyp	Ref	Expression
1		trclubgi.rex	|- R e. _V
2		trclublem	|- ( R e. _V -> ( R u. ( dom R X. ran R ) ) e. { s | ( R C_ s /\ ( s o. s ) C_ s ) } )
3		intss1	|- ( ( R u. ( 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_ ( R u. ( dom R X. ran R ) ) )
4	1 2 3	mp2b	|- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( R u. ( dom R X. ran R ) )