relbrcoss

Description: A and B are cosets by relation R : a binary relation. (Contributed by Peter Mazsa, 22-Apr-2021)

		Ref	Expression
	Assertion	relbrcoss	$⊢ (A \in V \land B \in W) \to (Rel R \to (A ≀ R B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R)))$

Step	Hyp	Ref	Expression
1		resdm	$⊢ Rel R \to {R ↾}_{dom R} = R$
2	1	cosseqd	$⊢ Rel R \to ≀ ({R ↾}_{dom R}) = ≀ R$
3	2	breqd	$⊢ Rel R \to (A ≀ ({R ↾}_{dom R}) B \leftrightarrow A ≀ R B)$
4	3	adantl	$⊢ ((A \in V \land B \in W) \land Rel R) \to (A ≀ ({R ↾}_{dom R}) B \leftrightarrow A ≀ R B)$
5		br1cossres2	$⊢ (A \in V \land B \in W) \to (A ≀ ({R ↾}_{dom R}) B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R))$
6	5	adantr	$⊢ ((A \in V \land B \in W) \land Rel R) \to (A ≀ ({R ↾}_{dom R}) B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R))$
7	4 6	bitr3d	$⊢ ((A \in V \land B \in W) \land Rel R) \to (A ≀ R B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R))$
8	7	ex	$⊢ (A \in V \land B \in W) \to (Rel R \to (A ≀ R B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R)))$

Metamath Proof Explorer