Theorem trrelsuperreldg

Description: Concrete construction of a superclass of relation R which is a transitive relation. (Contributed by RP, 25-Dec-2019)

	Ref	Expression
Hypotheses	trrelsuperreldg.r	|- ( ph -> Rel R )
	trrelsuperreldg.s	|- ( ph -> S = ( dom R X. ran R ) )
Assertion	trrelsuperreldg	|- ( ph -> ( R C_ S /\ ( S o. S ) C_ S ) )

Proof

Step	Hyp	Ref	Expression
1		trrelsuperreldg.r	|- ( ph -> Rel R )
2		trrelsuperreldg.s	|- ( ph -> S = ( dom R X. ran R ) )
3		relssdmrn	|- ( Rel R -> R C_ ( dom R X. ran R ) )
4	1 3	syl	|- ( ph -> R C_ ( dom R X. ran R ) )
5	4 2	sseqtrrd	|- ( ph -> R C_ S )
6		xptrrel	|- ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( dom R X. ran R )
7	6	a1i	|- ( ph -> ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( dom R X. ran R ) )
8	2 2	coeq12d	|- ( ph -> ( S o. S ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
9	7 8 2	3sstr4d	|- ( ph -> ( S o. S ) C_ S )
10	5 9	jca	|- ( ph -> ( R C_ S /\ ( S o. S ) C_ S ) )