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

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

Proof

Step Hyp Ref Expression
1 brcnvg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑢 ∈ V ) → ( 𝐴 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝐴 ) )
2 1 elvd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝐴 ) )
3 brcnvg ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑢 ∈ V ) → ( 𝐵 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝐵 ) )
4 3 elvd ⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝐵 ) )
5 2 4 bi2anan9 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ◡ 𝑅 𝑢 ∧ 𝐵 ◡ 𝑅 𝑢 ) ↔ ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) )
6 5 exbidv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑢 ( 𝐴 ◡ 𝑅 𝑢 ∧ 𝐵 ◡ 𝑅 𝑢 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) )
7 ecinn0 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ◡ 𝑅 ∩ [ 𝐵 ] ◡ 𝑅 ) ≠ ∅ ↔ ∃ 𝑢 ( 𝐴 ◡ 𝑅 𝑢 ∧ 𝐵 ◡ 𝑅 𝑢 ) ) )
8 brcoss ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) )
9 6 7 8 3bitr4rd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ( [ 𝐴 ] ◡ 𝑅 ∩ [ 𝐵 ] ◡ 𝑅 ) ≠ ∅ ) )