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 \leftrightarrow (\forall u \in dom R \forall v \in dom R ([u] R \cap [v] R \neq \emptyset \to u = v) \land Rel R)$

Proof

Step	Hyp	Ref	Expression
1		dfdisjALTV5	$⊢ Disj R \leftrightarrow (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land Rel R)$
2		orcom	$⊢ (u = v \lor [u] R \cap [v] R = \emptyset) \leftrightarrow ([u] R \cap [v] R = \emptyset \lor u = v)$
3		neor	$⊢ ([u] R \cap [v] R = \emptyset \lor u = v) \leftrightarrow ([u] R \cap [v] R \neq \emptyset \to u = v)$
4	2 3	bitri	$⊢ (u = v \lor [u] R \cap [v] R = \emptyset) \leftrightarrow ([u] R \cap [v] R \neq \emptyset \to u = v)$
5	4	2ralbii	$⊢ \forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \leftrightarrow \forall u \in dom R \forall v \in dom R ([u] R \cap [v] R \neq \emptyset \to u = v)$
6	1 5	bianbi	$⊢ Disj R \leftrightarrow (\forall u \in dom R \forall v \in dom R ([u] R \cap [v] R \neq \emptyset \to u = v) \land Rel R)$

Metamath Proof Explorer

Theorem dfdisjALTV5a

Proof