Metamath Proof Explorer


Theorem eleccossin

Description: Two ways of saying that the coset of A and the coset of C have the common element B . (Contributed by Peter Mazsa, 15-Oct-2021)

Ref Expression
Assertion eleccossin ( ( 𝐵𝑉𝐶𝑊 ) → ( 𝐵 ∈ ( [ 𝐴 ] ≀ 𝑅 ∩ [ 𝐶 ] ≀ 𝑅 ) ↔ ( 𝐴𝑅 𝐵𝐵𝑅 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 elin ( 𝐵 ∈ ( [ 𝐴 ] ≀ 𝑅 ∩ [ 𝐶 ] ≀ 𝑅 ) ↔ ( 𝐵 ∈ [ 𝐴 ] ≀ 𝑅𝐵 ∈ [ 𝐶 ] ≀ 𝑅 ) )
2 relcoss Rel ≀ 𝑅
3 relelec ( Rel ≀ 𝑅 → ( 𝐵 ∈ [ 𝐴 ] ≀ 𝑅𝐴𝑅 𝐵 ) )
4 2 3 ax-mp ( 𝐵 ∈ [ 𝐴 ] ≀ 𝑅𝐴𝑅 𝐵 )
5 relelec ( Rel ≀ 𝑅 → ( 𝐵 ∈ [ 𝐶 ] ≀ 𝑅𝐶𝑅 𝐵 ) )
6 2 5 ax-mp ( 𝐵 ∈ [ 𝐶 ] ≀ 𝑅𝐶𝑅 𝐵 )
7 4 6 anbi12i ( ( 𝐵 ∈ [ 𝐴 ] ≀ 𝑅𝐵 ∈ [ 𝐶 ] ≀ 𝑅 ) ↔ ( 𝐴𝑅 𝐵𝐶𝑅 𝐵 ) )
8 1 7 bitri ( 𝐵 ∈ ( [ 𝐴 ] ≀ 𝑅 ∩ [ 𝐶 ] ≀ 𝑅 ) ↔ ( 𝐴𝑅 𝐵𝐶𝑅 𝐵 ) )
9 brcosscnvcoss ( ( 𝐵𝑉𝐶𝑊 ) → ( 𝐵𝑅 𝐶𝐶𝑅 𝐵 ) )
10 9 anbi2d ( ( 𝐵𝑉𝐶𝑊 ) → ( ( 𝐴𝑅 𝐵𝐵𝑅 𝐶 ) ↔ ( 𝐴𝑅 𝐵𝐶𝑅 𝐵 ) ) )
11 8 10 bitr4id ( ( 𝐵𝑉𝐶𝑊 ) → ( 𝐵 ∈ ( [ 𝐴 ] ≀ 𝑅 ∩ [ 𝐶 ] ≀ 𝑅 ) ↔ ( 𝐴𝑅 𝐵𝐵𝑅 𝐶 ) ) )