dfdisjs5

Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021)

		Ref	Expression
	Assertion	dfdisjs5	$⊢ Disjs = \{r \in Rels \| \forall u \in dom r \forall v \in dom r (u = v \lor [u] r \cap [v] r = \emptyset)\}$

Step	Hyp	Ref	Expression
1		dfdisjs2	$⊢ Disjs = \{r \in Rels \| ≀ r^{-1} \subseteq I\}$
2		cosscnvssid5	$⊢ (≀ r^{-1} \subseteq I \land Rel r) \leftrightarrow (\forall u \in dom r \forall v \in dom r (u = v \lor [u] r \cap [v] r = \emptyset) \land Rel r)$
3		elrelsrelim	$⊢ r \in Rels \to Rel r$
4	3	biantrud	$⊢ r \in Rels \to (≀ r^{-1} \subseteq I \leftrightarrow (≀ r^{-1} \subseteq I \land Rel r))$
5	3	biantrud	$⊢ r \in Rels \to (\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 = v \lor [u] r \cap [v] r = \emptyset) \land Rel r))$
6	4 5	bibi12d	$⊢ r \in Rels \to ((≀ r^{-1} \subseteq I \leftrightarrow \forall u \in dom r \forall v \in dom r (u = v \lor [u] r \cap [v] r = \emptyset)) \leftrightarrow ((≀ r^{-1} \subseteq I \land Rel r) \leftrightarrow (\forall u \in dom r \forall v \in dom r (u = v \lor [u] r \cap [v] r = \emptyset) \land Rel r)))$
7	2 6	mpbiri	$⊢ r \in Rels \to (≀ r^{-1} \subseteq I \leftrightarrow \forall u \in dom r \forall v \in dom r (u = v \lor [u] r \cap [v] r = \emptyset))$
8	1 7	rabimbieq	$⊢ Disjs = \{r \in Rels \| \forall u \in dom r \forall v \in dom r (u = v \lor [u] r \cap [v] r = \emptyset)\}$

Metamath Proof Explorer