# Metamath Proof Explorer

## 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}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\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}×\mathrm{V}\right)$
2 incom ${⊢}\bigcap \left\{{x}|{\phi }\right\}\cap \left(\mathrm{V}×\mathrm{V}\right)=\left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}$
3 1 2 eqtri ${⊢}{{\bigcap \left\{{x}|{\phi }\right\}}^{-1}}^{-1}=\left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}$
4 dfrel2 ${⊢}\mathrm{Rel}\bigcap \left\{{x}|{\phi }\right\}↔{{\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}\phantom{\rule{.4em}{0ex}}{\phi }$
7 6 xpinintabd ${⊢}\mathrm{Rel}\bigcap \left\{{x}|{\phi }\right\}\to \left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}=\bigcap \left\{{w}\in 𝒫\left(\mathrm{V}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}=\left(\mathrm{V}×\mathrm{V}\right)\cap {x}\wedge {\phi }\right)\right\}$
8 incom ${⊢}\left(\mathrm{V}×\mathrm{V}\right)\cap {x}={x}\cap \left(\mathrm{V}×\mathrm{V}\right)$
9 cnvcnv ${⊢}{{{x}}^{-1}}^{-1}={x}\cap \left(\mathrm{V}×\mathrm{V}\right)$
10 8 9 eqtr4i ${⊢}\left(\mathrm{V}×\mathrm{V}\right)\cap {x}={{{x}}^{-1}}^{-1}$
11 10 eqeq2i ${⊢}{w}=\left(\mathrm{V}×\mathrm{V}\right)\cap {x}↔{w}={{{x}}^{-1}}^{-1}$
12 11 anbi1i ${⊢}\left({w}=\left(\mathrm{V}×\mathrm{V}\right)\cap {x}\wedge {\phi }\right)↔\left({w}={{{x}}^{-1}}^{-1}\wedge {\phi }\right)$
13 12 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}=\left(\mathrm{V}×\mathrm{V}\right)\cap {x}\wedge {\phi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}={{{x}}^{-1}}^{-1}\wedge {\phi }\right)$
14 13 rabbii ${⊢}\left\{{w}\in 𝒫\left(\mathrm{V}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}=\left(\mathrm{V}×\mathrm{V}\right)\cap {x}\wedge {\phi }\right)\right\}=\left\{{w}\in 𝒫\left(\mathrm{V}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}={{{x}}^{-1}}^{-1}\wedge {\phi }\right)\right\}$
15 14 inteqi ${⊢}\bigcap \left\{{w}\in 𝒫\left(\mathrm{V}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}=\left(\mathrm{V}×\mathrm{V}\right)\cap {x}\wedge {\phi }\right)\right\}=\bigcap \left\{{w}\in 𝒫\left(\mathrm{V}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}={{{x}}^{-1}}^{-1}\wedge {\phi }\right)\right\}$
16 7 15 syl6eq ${⊢}\mathrm{Rel}\bigcap \left\{{x}|{\phi }\right\}\to \left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}=\bigcap \left\{{w}\in 𝒫\left(\mathrm{V}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\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}×\mathrm{V}\right)|\exists {x}\phantom{\rule{.4em}{0ex}}\left({w}={{{x}}^{-1}}^{-1}\wedge {\phi }\right)\right\}$