Metamath Proof Explorer

Theorem dfdisjALTV5

Description: Alternate definition of the disjoint relation predicate, cf. dffunALTV5 . (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion dfdisjALTV5 ⊢ Disj R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 dfdisjALTV2 ⊢ Disj R ↔ ≀ R -1 ⊆ I ∧ Rel ⁡ R
2 cosscnvssid5 ⊢ ≀ R -1 ⊆ I ∧ Rel ⁡ R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R
3 1 2 bitri ⊢ Disj R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R