Theorem cnviun

Description: Converse of indexed union. (Contributed by RP, 20-Jun-2020)

	Ref	Expression
Assertion	cnviun	$$⊢{\bigcup _{x\in A}B}^{-1}=\bigcup _{x\in A}{B}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\bigcup _{x\in A}B}^{-1}$$
2		reliun	$$⊢\mathrm{Rel}\bigcup _{x\in A}{B}^{-1}\leftrightarrow \forall x\in A\mathrm{Rel}{B}^{-1}$$
3		relcnv	$$⊢\mathrm{Rel}{B}^{-1}$$
4	3	a1i	$$⊢x\in A\to \mathrm{Rel}{B}^{-1}$$
5	2 4	mprgbir	$$⊢\mathrm{Rel}\bigcup _{x\in A}{B}^{-1}$$
6		vex	$$⊢y\in \mathrm{V}$$
7		vex	$$⊢z\in \mathrm{V}$$
8	6 7	opelcnv	$$⊢⟨y,z⟩\in B^{-1}\leftrightarrow ⟨z,y⟩\in B$$
9	8	bicomi	$$⊢⟨z,y⟩\in B\leftrightarrow ⟨y,z⟩\in B^{-1}$$
10	9	rexbii	$$⊢\exists x\in A⟨z,y⟩\in B\leftrightarrow \exists x\in A⟨y,z⟩\in B^{-1}$$
11	6 7	opelcnv	$$⊢⟨y,z⟩\in {\bigcup _{x\in A}B}^{-1}\leftrightarrow ⟨z,y⟩\in \bigcup _{x\in A}B$$
12		eliun	$$⊢⟨z,y⟩\in \bigcup _{x\in A}B\leftrightarrow \exists x\in A⟨z,y⟩\in B$$
13	11 12	bitri	$$⊢⟨y,z⟩\in {\bigcup _{x\in A}B}^{-1}\leftrightarrow \exists x\in A⟨z,y⟩\in B$$
14		eliun	$$⊢⟨y,z⟩\in \bigcup _{x\in A}{B}^{-1}\leftrightarrow \exists x\in A⟨y,z⟩\in B^{-1}$$
15	10 13 14	3bitr4i	$$⊢⟨y,z⟩\in {\bigcup _{x\in A}B}^{-1}\leftrightarrow ⟨y,z⟩\in \bigcup _{x\in A}{B}^{-1}$$
16	1 5 15	eqrelriiv	$$⊢{\bigcup _{x\in A}B}^{-1}=\bigcup _{x\in A}{B}^{-1}$$