This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ∈ ( [ 𝐴 ] ≀ 𝑅 ∩ [ 𝐶 ] ≀ 𝑅 ) ↔ ( 𝐴 ≀ 𝑅 𝐵 ∧ 𝐵 ≀ 𝑅 𝐶 ) ) )