Theorem cnviin

Description: The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Assertion	cnviin	$$⊢A\ne \varnothing \to {\bigcap _{x\in A}B}^{-1}=\bigcap _{x\in A}{B}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\bigcap _{x\in A}B}^{-1}$$
2		relcnv	$$⊢\mathrm{Rel}{B}^{-1}$$
3		df-rel	$$⊢\mathrm{Rel}{B}^{-1}\leftrightarrow B^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
4	2 3	mpbi	$$⊢B^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
5	4	rgenw	$$⊢\forall x\in A{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
6		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall x\in A{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}\right)\to \exists x\in A{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
7	5 6	mpan2	$$⊢A\ne \varnothing \to \exists x\in A{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
8		iinss	$$⊢\exists x\in A{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}\to \bigcap _{x\in A}{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
9	7 8	syl	$$⊢A\ne \varnothing \to \bigcap _{x\in A}{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
10		df-rel	$$⊢\mathrm{Rel}\bigcap _{x\in A}{B}^{-1}\leftrightarrow \bigcap _{x\in A}{B}^{-1}\subseteq \mathrm{V}\times \mathrm{V}$$
11	9 10	sylibr	$$⊢A\ne \varnothing \to \mathrm{Rel}\bigcap _{x\in A}{B}^{-1}$$
12		opex	$$⊢⟨b,a⟩\in \mathrm{V}$$
13		eliin	$$⊢⟨b,a⟩\in \mathrm{V}\to \left(⟨b,a⟩\in \bigcap _{x\in A}B\leftrightarrow \forall x\in A⟨b,a⟩\in B\right)$$
14	12 13	ax-mp	$$⊢⟨b,a⟩\in \bigcap _{x\in A}B\leftrightarrow \forall x\in A⟨b,a⟩\in B$$
15		vex	$$⊢a\in \mathrm{V}$$
16		vex	$$⊢b\in \mathrm{V}$$
17	15 16	opelcnv	$$⊢⟨a,b⟩\in {\bigcap _{x\in A}B}^{-1}\leftrightarrow ⟨b,a⟩\in \bigcap _{x\in A}B$$
18		opex	$$⊢⟨a,b⟩\in \mathrm{V}$$
19		eliin	$$⊢⟨a,b⟩\in \mathrm{V}\to \left(⟨a,b⟩\in \bigcap _{x\in A}{B}^{-1}\leftrightarrow \forall x\in A⟨a,b⟩\in B^{-1}\right)$$
20	18 19	ax-mp	$$⊢⟨a,b⟩\in \bigcap _{x\in A}{B}^{-1}\leftrightarrow \forall x\in A⟨a,b⟩\in B^{-1}$$
21	15 16	opelcnv	$$⊢⟨a,b⟩\in B^{-1}\leftrightarrow ⟨b,a⟩\in B$$
22	21	ralbii	$$⊢\forall x\in A⟨a,b⟩\in B^{-1}\leftrightarrow \forall x\in A⟨b,a⟩\in B$$
23	20 22	bitri	$$⊢⟨a,b⟩\in \bigcap _{x\in A}{B}^{-1}\leftrightarrow \forall x\in A⟨b,a⟩\in B$$
24	14 17 23	3bitr4i	$$⊢⟨a,b⟩\in {\bigcap _{x\in A}B}^{-1}\leftrightarrow ⟨a,b⟩\in \bigcap _{x\in A}{B}^{-1}$$
25	24	eqrelriv	$$⊢\left(\mathrm{Rel}{\bigcap _{x\in A}B}^{-1}\wedge \mathrm{Rel}\bigcap _{x\in A}{B}^{-1}\right)\to {\bigcap _{x\in A}B}^{-1}=\bigcap _{x\in A}{B}^{-1}$$
26	1 11 25	sylancr	$$⊢A\ne \varnothing \to {\bigcap _{x\in A}B}^{-1}=\bigcap _{x\in A}{B}^{-1}$$