ecxrn2

Description: The ( R |X. S ) -coset of a set is the Cartesian product of its R -coset and S -coset. (Contributed by Peter Mazsa, 16-Oct-2020)

		Ref	Expression
	Assertion	ecxrn2	$⊢ A \in V \to [A] R ⋉ S = [A] R \times [A] S$

Step	Hyp	Ref	Expression
1		relecxrn	$⊢ A \in V \to Rel [A] R ⋉ S$
2		relxp	$⊢ Rel ([A] R \times [A] S)$
3	1 2	jctir	$⊢ A \in V \to (Rel [A] R ⋉ S \land Rel ([A] R \times [A] S))$
4		brxrn	$⊢ (A \in V \land x \in V \land y \in V) \to (A R ⋉ S ⟨x, y⟩ \leftrightarrow (A R x \land A S y))$
5	4	el3v23	$⊢ A \in V \to (A R ⋉ S ⟨x, y⟩ \leftrightarrow (A R x \land A S y))$
6		opex	$⊢ ⟨x, y⟩ \in V$
7		elecALTV	$⊢ (A \in V \land ⟨x, y⟩ \in V) \to (⟨x, y⟩ \in [A] R ⋉ S \leftrightarrow A R ⋉ S ⟨x, y⟩)$
8	6 7	mpan2	$⊢ A \in V \to (⟨x, y⟩ \in [A] R ⋉ S \leftrightarrow A R ⋉ S ⟨x, y⟩)$
9		elecALTV	$⊢ (A \in V \land x \in V) \to (x \in [A] R \leftrightarrow A R x)$
10	9	elvd	$⊢ A \in V \to (x \in [A] R \leftrightarrow A R x)$
11		elecALTV	$⊢ (A \in V \land y \in V) \to (y \in [A] S \leftrightarrow A S y)$
12	11	elvd	$⊢ A \in V \to (y \in [A] S \leftrightarrow A S y)$
13	10 12	anbi12d	$⊢ A \in V \to ((x \in [A] R \land y \in [A] S) \leftrightarrow (A R x \land A S y))$
14	5 8 13	3bitr4d	$⊢ A \in V \to (⟨x, y⟩ \in [A] R ⋉ S \leftrightarrow (x \in [A] R \land y \in [A] S))$
15		opelxp	$⊢ ⟨x, y⟩ \in ([A] R \times [A] S) \leftrightarrow (x \in [A] R \land y \in [A] S)$
16	14 15	bitr4di	$⊢ A \in V \to (⟨x, y⟩ \in [A] R ⋉ S \leftrightarrow ⟨x, y⟩ \in ([A] R \times [A] S))$
17	16	eqrelrdv2	$⊢ ((Rel [A] R ⋉ S \land Rel ([A] R \times [A] S)) \land A \in V) \to [A] R ⋉ S = [A] R \times [A] S$
18	3 17	mpancom	$⊢ A \in V \to [A] R ⋉ S = [A] R \times [A] S$

Metamath Proof Explorer