Metamath Proof Explorer

Theorem brcoss3

Description: Alternate form of the A and B are cosets by R binary relation. (Contributed by Peter Mazsa, 26-Mar-2019)

Ref Expression
Assertion brcoss3 ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ A R -1 ∩ B R -1 ≠ ∅

Proof

Step Hyp Ref Expression
1 brcnvg ⊢ A ∈ V ∧ u ∈ V → A R -1 u ↔ u R A
2 1 elvd ⊢ A ∈ V → A R -1 u ↔ u R A
3 brcnvg ⊢ B ∈ W ∧ u ∈ V → B R -1 u ↔ u R B
4 3 elvd ⊢ B ∈ W → B R -1 u ↔ u R B
5 2 4 bi2anan9 ⊢ A ∈ V ∧ B ∈ W → A R -1 u ∧ B R -1 u ↔ u R A ∧ u R B
6 5 exbidv ⊢ A ∈ V ∧ B ∈ W → ∃ u A R -1 u ∧ B R -1 u ↔ ∃ u u R A ∧ u R B
7 ecinn0 ⊢ A ∈ V ∧ B ∈ W → A R -1 ∩ B R -1 ≠ ∅ ↔ ∃ u A R -1 u ∧ B R -1 u
8 brcoss ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ ∃ u u R A ∧ u R B
9 6 7 8 3bitr4rd ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ A R -1 ∩ B R -1 ≠ ∅