eldisjs5

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

		Ref	Expression
	Assertion	eldisjs5	$⊢ R \in V \to (R \in Disjs \leftrightarrow (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land R \in Rels))$

Step	Hyp	Ref	Expression
1		eldisjs2	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \subseteq I \land R \in Rels)$
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		elrelsrel	$⊢ R \in V \to (R \in Rels \leftrightarrow Rel R)$
4	3	anbi2d	$⊢ R \in V \to ((≀ R^{-1} \subseteq I \land R \in Rels) \leftrightarrow (≀ R^{-1} \subseteq I \land Rel R))$
5	3	anbi2d	$⊢ R \in V \to ((\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land R \in Rels) \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 V \to (((≀ R^{-1} \subseteq I \land R \in Rels) \leftrightarrow (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land R \in Rels)) \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 V \to ((≀ R^{-1} \subseteq I \land R \in Rels) \leftrightarrow (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land R \in Rels))$
8	1 7	bitrid	$⊢ R \in V \to (R \in Disjs \leftrightarrow (\forall u \in dom R \forall v \in dom R (u = v \lor [u] R \cap [v] R = \emptyset) \land R \in Rels))$

Metamath Proof Explorer