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	$⊢ ≀ {A ⋉ B}^{-1} = ≀ A^{-1} \cap ≀ B^{-1}$

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

Metamath Proof Explorer