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

Metamath Proof Explorer

Theorem cosscnv

Description: Class of cosets by the converse of R (Contributed by Peter Mazsa, 17-Jun-2020)

Ref Expression
Assertion cosscnv ≀ ◡ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 𝑅 𝑢 ∧ 𝑦 𝑅 𝑢 ) }

Proof

Step Hyp Ref Expression
1 df-coss ⊢ ≀ ◡ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 ◡ 𝑅 𝑥 ∧ 𝑢 ◡ 𝑅 𝑦 ) }
2 brcnvg ⊢ ( ( 𝑢 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑢 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑢 ) )
3 2 el2v ⊢ ( 𝑢 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑢 )
4 brcnvg ⊢ ( ( 𝑢 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑢 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑢 ) )
5 4 el2v ⊢ ( 𝑢 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑢 )
6 3 5 anbi12i ⊢ ( ( 𝑢 ◡ 𝑅 𝑥 ∧ 𝑢 ◡ 𝑅 𝑦 ) ↔ ( 𝑥 𝑅 𝑢 ∧ 𝑦 𝑅 𝑢 ) )
7 6 exbii ⊢ ( ∃ 𝑢 ( 𝑢 ◡ 𝑅 𝑥 ∧ 𝑢 ◡ 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑥 𝑅 𝑢 ∧ 𝑦 𝑅 𝑢 ) )
8 7 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 ◡ 𝑅 𝑥 ∧ 𝑢 ◡ 𝑅 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 𝑅 𝑢 ∧ 𝑦 𝑅 𝑢 ) }
9 1 8 eqtri ⊢ ≀ ◡ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 𝑅 𝑢 ∧ 𝑦 𝑅 𝑢 ) }