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	$$⊢\phi \to \mathrm{Rel}R$$
	trrelsuperreldg.s	$$⊢\phi \to S=\mathrm{dom}R\times \mathrm{ran}R$$
Assertion	trrelsuperreldg	$$⊢\phi \to \left(R\subseteq S\wedge S\circ S\subseteq S\right)$$

Proof

Step	Hyp	Ref	Expression
1		trrelsuperreldg.r	$$⊢\phi \to \mathrm{Rel}R$$
2		trrelsuperreldg.s	$$⊢\phi \to S=\mathrm{dom}R\times \mathrm{ran}R$$
3		relssdmrn	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
4	1 3	syl	$$⊢\phi \to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
5	4 2	sseqtrrd	$$⊢\phi \to R\subseteq S$$
6		xptrrel	$$⊢\left(\mathrm{dom}R\times \mathrm{ran}R\right)\circ \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
7	6	a1i	$$⊢\phi \to \left(\mathrm{dom}R\times \mathrm{ran}R\right)\circ \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
8	2 2	coeq12d	$$⊢\phi \to S\circ S=\left(\mathrm{dom}R\times \mathrm{ran}R\right)\circ \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
9	7 8 2	3sstr4d	$$⊢\phi \to S\circ S\subseteq S$$
10	5 9	jca	$$⊢\phi \to \left(R\subseteq S\wedge S\circ S\subseteq S\right)$$