Theorem 1cosscnvxrn

Description: Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

	Ref	Expression
Assertion	1cosscnvxrn	$$⊢\wr {A⋉B}^{-1}=\wr A^{-1}\cap \wr B^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		br1cosscnvxrn	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(x\wr {A⋉B}^{-1}y\leftrightarrow \left(x\wr A^{-1}y\wedge x\wr B^{-1}y\right)\right)$$
2	1	el2v	$$⊢x\wr {A⋉B}^{-1}y\leftrightarrow \left(x\wr A^{-1}y\wedge x\wr B^{-1}y\right)$$
3	2	opabbii	$$⊢\left\{⟨x,y⟩|x\wr {A⋉B}^{-1}y\right\}=\left\{⟨x,y⟩|\left(x\wr A^{-1}y\wedge x\wr B^{-1}y\right)\right\}$$
4		inopab	$$⊢\left\{⟨x,y⟩|x\wr A^{-1}y\right\}\cap \left\{⟨x,y⟩|x\wr B^{-1}y\right\}=\left\{⟨x,y⟩|\left(x\wr A^{-1}y\wedge x\wr B^{-1}y\right)\right\}$$
5	3 4	eqtr4i	$$⊢\left\{⟨x,y⟩|x\wr {A⋉B}^{-1}y\right\}=\left\{⟨x,y⟩|x\wr A^{-1}y\right\}\cap \left\{⟨x,y⟩|x\wr B^{-1}y\right\}$$
6		relcoss	$$⊢\mathrm{Rel}\wr {A⋉B}^{-1}$$
7		dfrel4v	$$⊢\mathrm{Rel}\wr {A⋉B}^{-1}\leftrightarrow \wr {A⋉B}^{-1}=\left\{⟨x,y⟩|x\wr {A⋉B}^{-1}y\right\}$$
8	6 7	mpbi	$$⊢\wr {A⋉B}^{-1}=\left\{⟨x,y⟩|x\wr {A⋉B}^{-1}y\right\}$$
9		relcoss	$$⊢\mathrm{Rel}\wr A^{-1}$$
10		dfrel4v	$$⊢\mathrm{Rel}\wr A^{-1}\leftrightarrow \wr A^{-1}=\left\{⟨x,y⟩|x\wr A^{-1}y\right\}$$
11	9 10	mpbi	$$⊢\wr A^{-1}=\left\{⟨x,y⟩|x\wr A^{-1}y\right\}$$
12		relcoss	$$⊢\mathrm{Rel}\wr B^{-1}$$
13		dfrel4v	$$⊢\mathrm{Rel}\wr B^{-1}\leftrightarrow \wr B^{-1}=\left\{⟨x,y⟩|x\wr B^{-1}y\right\}$$
14	12 13	mpbi	$$⊢\wr B^{-1}=\left\{⟨x,y⟩|x\wr B^{-1}y\right\}$$
15	11 14	ineq12i	$$⊢\wr A^{-1}\cap \wr B^{-1}=\left\{⟨x,y⟩|x\wr A^{-1}y\right\}\cap \left\{⟨x,y⟩|x\wr B^{-1}y\right\}$$
16	5 8 15	3eqtr4i	$$⊢\wr {A⋉B}^{-1}=\wr A^{-1}\cap \wr B^{-1}$$