Metamath Proof Explorer

Theorem cosscnvssid5

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

Ref Expression
Assertion cosscnvssid5 ⊢ ≀ R -1 ⊆ I ∧ Rel ⁡ R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 cosscnvssid4 ⊢ ≀ R -1 ⊆ I ↔ ∀ x ∃* u u R x
2 1 anbi1i ⊢ ≀ R -1 ⊆ I ∧ Rel ⁡ R ↔ ∀ x ∃* u u R x ∧ Rel ⁡ R
3 inecmo3 ⊢ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R ↔ ∀ x ∃* u u R x ∧ Rel ⁡ R
4 2 3 bitr4i ⊢ ≀ R -1 ⊆ I ∧ Rel ⁡ R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R