Theorem clrellem

Description: When the property ps holds for a relation substituted for x , then the closure on that property is a relation if the base set is a relation. (Contributed by RP, 30-Jul-2020)

	Ref	Expression
Hypotheses	clrellem.y	$$⊢\phi \to Y\in \mathrm{V}$$
	clrellem.rel	$$⊢\phi \to \mathrm{Rel}X$$
	clrellem.sub	$$⊢x={Y^{-1}}^{-1}\to \left(\psi \leftrightarrow \chi \right)$$
	clrellem.sup	$$⊢\phi \to X\subseteq Y$$
	clrellem.maj	$$⊢\phi \to \chi$$
Assertion	clrellem	$$⊢\phi \to \mathrm{Rel}\bigcap \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		clrellem.y	$$⊢\phi \to Y\in \mathrm{V}$$
2		clrellem.rel	$$⊢\phi \to \mathrm{Rel}X$$
3		clrellem.sub	$$⊢x={Y^{-1}}^{-1}\to \left(\psi \leftrightarrow \chi \right)$$
4		clrellem.sup	$$⊢\phi \to X\subseteq Y$$
5		clrellem.maj	$$⊢\phi \to \chi$$
6		cnvexg	$$⊢Y\in \mathrm{V}\to Y^{-1}\in \mathrm{V}$$
7		cnvexg	$$⊢Y^{-1}\in \mathrm{V}\to {Y^{-1}}^{-1}\in \mathrm{V}$$
8	1 6 7	3syl	$$⊢\phi \to {Y^{-1}}^{-1}\in \mathrm{V}$$
9		dfrel2	$$⊢\mathrm{Rel}X\leftrightarrow {X^{-1}}^{-1}=X$$
10	2 9	sylib	$$⊢\phi \to {X^{-1}}^{-1}=X$$
11		cnvss	$$⊢X\subseteq Y\to X^{-1}\subseteq Y^{-1}$$
12		cnvss	$$⊢X^{-1}\subseteq Y^{-1}\to {X^{-1}}^{-1}\subseteq {Y^{-1}}^{-1}$$
13	4 11 12	3syl	$$⊢\phi \to {X^{-1}}^{-1}\subseteq {Y^{-1}}^{-1}$$
14	10 13	eqsstrrd	$$⊢\phi \to X\subseteq {Y^{-1}}^{-1}$$
15		relcnv	$$⊢\mathrm{Rel}{Y^{-1}}^{-1}$$
16	15	a1i	$$⊢\phi \to \mathrm{Rel}{Y^{-1}}^{-1}$$
17	14 5 16	jca31	$$⊢\phi \to \left(\left(X\subseteq {Y^{-1}}^{-1}\wedge \chi \right)\wedge \mathrm{Rel}{Y^{-1}}^{-1}\right)$$
18	3	cleq2lem	$$⊢x={Y^{-1}}^{-1}\to \left(\left(X\subseteq x\wedge \psi \right)\leftrightarrow \left(X\subseteq {Y^{-1}}^{-1}\wedge \chi \right)\right)$$
19		releq	$$⊢x={Y^{-1}}^{-1}\to \left(\mathrm{Rel}x\leftrightarrow \mathrm{Rel}{Y^{-1}}^{-1}\right)$$
20	18 19	anbi12d	$$⊢x={Y^{-1}}^{-1}\to \left(\left(\left(X\subseteq x\wedge \psi \right)\wedge \mathrm{Rel}x\right)\leftrightarrow \left(\left(X\subseteq {Y^{-1}}^{-1}\wedge \chi \right)\wedge \mathrm{Rel}{Y^{-1}}^{-1}\right)\right)$$
21	8 17 20	spcedv	$$⊢\phi \to \exists x\left(\left(X\subseteq x\wedge \psi \right)\wedge \mathrm{Rel}x\right)$$
22		releq	$$⊢y=x\to \left(\mathrm{Rel}y\leftrightarrow \mathrm{Rel}x\right)$$
23	22	rexab2	$$⊢\exists y\in \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}\mathrm{Rel}y\leftrightarrow \exists x\left(\left(X\subseteq x\wedge \psi \right)\wedge \mathrm{Rel}x\right)$$
24	23	biimpri	$$⊢\exists x\left(\left(X\subseteq x\wedge \psi \right)\wedge \mathrm{Rel}x\right)\to \exists y\in \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}\mathrm{Rel}y$$
25		relint	$$⊢\exists y\in \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}\mathrm{Rel}y\to \mathrm{Rel}\bigcap \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}$$
26	21 24 25	3syl	$$⊢\phi \to \mathrm{Rel}\bigcap \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}$$