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

Metamath Proof Explorer

Theorem cosscnvssid3

Description: Equivalent expressions for the class of cosets by the converse of R to be a subset of the identity class. (Contributed by Peter Mazsa, 28-Jul-2021)

Ref Expression
Assertion cosscnvssid3 ⊢ ≀ R -1 ⊆ I ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v

Proof

Step Hyp Ref Expression
1 cossssid3 ⊢ ≀ R -1 ⊆ I ↔ ∀ x ∀ u ∀ v x R -1 u ∧ x R -1 v → u = v
2 alrot3 ⊢ ∀ x ∀ u ∀ v x R -1 u ∧ x R -1 v → u = v ↔ ∀ u ∀ v ∀ x x R -1 u ∧ x R -1 v → u = v
3 brcnvg ⊢ x ∈ V ∧ u ∈ V → x R -1 u ↔ u R x
4 3 el2v ⊢ x R -1 u ↔ u R x
5 brcnvg ⊢ x ∈ V ∧ v ∈ V → x R -1 v ↔ v R x
6 5 el2v ⊢ x R -1 v ↔ v R x
7 4 6 anbi12i ⊢ x R -1 u ∧ x R -1 v ↔ u R x ∧ v R x
8 7 imbi1i ⊢ x R -1 u ∧ x R -1 v → u = v ↔ u R x ∧ v R x → u = v
9 8 3albii ⊢ ∀ u ∀ v ∀ x x R -1 u ∧ x R -1 v → u = v ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v
10 1 2 9 3bitri ⊢ ≀ R -1 ⊆ I ↔ ∀ u ∀ v ∀ x u R x ∧ v R x → u = v