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

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( Rel 𝑅 → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑥 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 resdm ⊢ ( Rel 𝑅 → ( 𝑅 ↾ dom 𝑅 ) = 𝑅 )
2 1 cosseqd ⊢ ( Rel 𝑅 → ≀ ( 𝑅 ↾ dom 𝑅 ) = ≀ 𝑅 )
3 2 breqd ⊢ ( Rel 𝑅 → ( 𝐴 ≀ ( 𝑅 ↾ dom 𝑅 ) 𝐵 ↔ 𝐴 ≀ 𝑅 𝐵 ) )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Rel 𝑅 ) → ( 𝐴 ≀ ( 𝑅 ↾ dom 𝑅 ) 𝐵 ↔ 𝐴 ≀ 𝑅 𝐵 ) )
5 br1cossres2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ ( 𝑅 ↾ dom 𝑅 ) 𝐵 ↔ ∃ 𝑥 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) )
6 5 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Rel 𝑅 ) → ( 𝐴 ≀ ( 𝑅 ↾ dom 𝑅 ) 𝐵 ↔ ∃ 𝑥 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) )
7 4 6 bitr3d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Rel 𝑅 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑥 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) )
8 7 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( Rel 𝑅 → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑥 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )