Theorem trclubNEW

Description: If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		trclubNEW.rex	|- ( ph -> R e. _V )
2		trclubNEW.rel	|- ( ph -> Rel R )
3	1	trclubgNEW	|- ( ph -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( R u. ( dom R X. ran R ) ) )
4		relssdmrn	|- ( Rel R -> R C_ ( dom R X. ran R ) )
5	2 4	syl	|- ( ph -> R C_ ( dom R X. ran R ) )
6		ssequn1	|- ( R C_ ( dom R X. ran R ) <-> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
7	5 6	sylib	|- ( ph -> ( R u. ( dom R X. ran R ) ) = ( dom R X. ran R ) )
8	3 7	sseqtrd	|- ( ph -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( dom R X. ran R ) )