Theorem relintab

Description: Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020)

	Ref	Expression
Assertion	relintab	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \bigcap \left\{x|\phi \right\}=\bigcap \left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w={x^{-1}}^{-1}\wedge \phi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnv	$$⊢{{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}=\bigcap \left\{x|\phi \right\}\cap \left(\mathrm{V}\times \mathrm{V}\right)$$
2		incom	$$⊢\bigcap \left\{x|\phi \right\}\cap \left(\mathrm{V}\times \mathrm{V}\right)=\left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}$$
3	1 2	eqtri	$$⊢{{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}=\left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}$$
4		dfrel2	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\leftrightarrow {{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}=\bigcap \left\{x|\phi \right\}$$
5	4	biimpi	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to {{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}=\bigcap \left\{x|\phi \right\}$$
6		relintabex	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \exists x\phi$$
7	6	xpinintabd	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}=\bigcap \left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w=\left(\mathrm{V}\times \mathrm{V}\right)\cap x\wedge \phi \right)\right\}$$
8		incom	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\cap x=x\cap \left(\mathrm{V}\times \mathrm{V}\right)$$
9		cnvcnv	$$⊢{x^{-1}}^{-1}=x\cap \left(\mathrm{V}\times \mathrm{V}\right)$$
10	8 9	eqtr4i	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\cap x={x^{-1}}^{-1}$$
11	10	eqeq2i	$$⊢w=\left(\mathrm{V}\times \mathrm{V}\right)\cap x\leftrightarrow w={x^{-1}}^{-1}$$
12	11	anbi1i	$$⊢\left(w=\left(\mathrm{V}\times \mathrm{V}\right)\cap x\wedge \phi \right)\leftrightarrow \left(w={x^{-1}}^{-1}\wedge \phi \right)$$
13	12	exbii	$$⊢\exists x\left(w=\left(\mathrm{V}\times \mathrm{V}\right)\cap x\wedge \phi \right)\leftrightarrow \exists x\left(w={x^{-1}}^{-1}\wedge \phi \right)$$
14	13	rabbii	$$⊢\left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w=\left(\mathrm{V}\times \mathrm{V}\right)\cap x\wedge \phi \right)\right\}=\left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w={x^{-1}}^{-1}\wedge \phi \right)\right\}$$
15	14	inteqi	$$⊢\bigcap \left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w=\left(\mathrm{V}\times \mathrm{V}\right)\cap x\wedge \phi \right)\right\}=\bigcap \left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w={x^{-1}}^{-1}\wedge \phi \right)\right\}$$
16	7 15	eqtrdi	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}=\bigcap \left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w={x^{-1}}^{-1}\wedge \phi \right)\right\}$$
17	3 5 16	3eqtr3a	$$⊢\mathrm{Rel}\bigcap \left\{x|\phi \right\}\to \bigcap \left\{x|\phi \right\}=\bigcap \left\{w\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(w={x^{-1}}^{-1}\wedge \phi \right)\right\}$$