Metamath Proof Explorer

Theorem dfdisjALTV5a

Description: Alternate definition of the disjoint relation predicate. Disj R means: different domain generators have disjoint cosets (unless the generators are equal), plus Rel R for relation-typedness. This is the characterization that makes canonicity/uniqueness arguments modular. It is the starting point for the entire " Disj <-> unique representative per block" pipeline that feeds into Disjs , see dfdisjs7 . (Contributed by Peter Mazsa, 3-Feb-2026)

Ref Expression
Assertion dfdisjALTV5a ⊢ Disj R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u R ∩ v R ≠ ∅ → u = v ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 dfdisjALTV5 ⊢ Disj R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R
2 orcom ⊢ u = v ∨ u R ∩ v R = ∅ ↔ u R ∩ v R = ∅ ∨ u = v
3 neor ⊢ u R ∩ v R = ∅ ∨ u = v ↔ u R ∩ v R ≠ ∅ → u = v
4 2 3 bitri ⊢ u = v ∨ u R ∩ v R = ∅ ↔ u R ∩ v R ≠ ∅ → u = v
5 4 2ralbii ⊢ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u R ∩ v R ≠ ∅ → u = v
6 1 5 bianbi ⊢ Disj R ↔ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u R ∩ v R ≠ ∅ → u = v ∧ Rel ⁡ R