Metamath Proof Explorer

Theorem 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 ∈ V ∧ B ∈ W → Rel ⁡ R → A ≀ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R

Proof

Step Hyp Ref Expression
1 resdm ⊢ Rel ⁡ R → R ↾ dom ⁡ R = R
2 1 cosseqd ⊢ Rel ⁡ R → ≀ R ↾ dom ⁡ R = ≀ R
3 2 breqd ⊢ Rel ⁡ R → A ≀ R ↾ dom ⁡ R B ↔ A ≀ R B
4 3 adantl ⊢ A ∈ V ∧ B ∈ W ∧ Rel ⁡ R → A ≀ R ↾ dom ⁡ R B ↔ A ≀ R B
5 br1cossres2 ⊢ A ∈ V ∧ B ∈ W → A ≀ R ↾ dom ⁡ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
6 5 adantr ⊢ A ∈ V ∧ B ∈ W ∧ Rel ⁡ R → A ≀ R ↾ dom ⁡ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
7 4 6 bitr3d ⊢ A ∈ V ∧ B ∈ W ∧ Rel ⁡ R → A ≀ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
8 7 ex ⊢ A ∈ V ∧ B ∈ W → Rel ⁡ R → A ≀ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R