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	$$⊢\phi \to R\in \mathrm{V}$$
	trclubNEW.rel	$$⊢\phi \to \mathrm{Rel}R$$
Assertion	trclubNEW	$$⊢\phi \to \bigcap \left\{x|\left(R\subseteq x\wedge x\circ x\subseteq x\right)\right\}\subseteq \mathrm{dom}R\times \mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		trclubNEW.rex	$$⊢\phi \to R\in \mathrm{V}$$
2		trclubNEW.rel	$$⊢\phi \to \mathrm{Rel}R$$
3	1	trclubgNEW	$$⊢\phi \to \bigcap \left\{x|\left(R\subseteq x\wedge x\circ x\subseteq x\right)\right\}\subseteq R\cup \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
4		relssdmrn	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
5	2 4	syl	$$⊢\phi \to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
6		ssequn1	$$⊢R\subseteq \mathrm{dom}R\times \mathrm{ran}R\leftrightarrow R\cup \left(\mathrm{dom}R\times \mathrm{ran}R\right)=\mathrm{dom}R\times \mathrm{ran}R$$
7	5 6	sylib	$$⊢\phi \to R\cup \left(\mathrm{dom}R\times \mathrm{ran}R\right)=\mathrm{dom}R\times \mathrm{ran}R$$
8	3 7	sseqtrd	$$⊢\phi \to \bigcap \left\{x|\left(R\subseteq x\wedge x\circ x\subseteq x\right)\right\}\subseteq \mathrm{dom}R\times \mathrm{ran}R$$