disjres

Description: Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023)

		Ref	Expression
	Assertion	disjres	$⊢ Rel R \to (Disj ({R ↾}_{A}) \leftrightarrow \forall u \in A \forall v \in A (u = v \lor [u] R \cap [v] R = \emptyset))$

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({R ↾}_{A})$
2		dfdisjALTV4	$⊢ Disj ({R ↾}_{A}) \leftrightarrow (\forall x \exists^{*} u u ({R ↾}_{A}) x \land Rel ({R ↾}_{A}))$
3	1 2	mpbiran2	$⊢ Disj ({R ↾}_{A}) \leftrightarrow \forall x \exists^{*} u u ({R ↾}_{A}) x$
4		brres	$⊢ x \in V \to (u ({R ↾}_{A}) x \leftrightarrow (u \in A \land u R x))$
5	4	elv	$⊢ u ({R ↾}_{A}) x \leftrightarrow (u \in A \land u R x)$
6	5	mobii	$⊢ \exists^{} u u ({R ↾}_{A}) x \leftrightarrow \exists^{} u (u \in A \land u R x)$
7		df-rmo	$⊢ \exists^{} u \in A u R x \leftrightarrow \exists^{} u (u \in A \land u R x)$
8	6 7	bitr4i	$⊢ \exists^{} u u ({R ↾}_{A}) x \leftrightarrow \exists^{} u \in A u R x$
9	8	albii	$⊢ \forall x \exists^{} u u ({R ↾}_{A}) x \leftrightarrow \forall x \exists^{} u \in A u R x$
10	3 9	bitri	$⊢ Disj ({R ↾}_{A}) \leftrightarrow \forall x \exists^{*} u \in A u R x$
11		id	$⊢ u = v \to u = v$
12	11	inecmo	$⊢ Rel R \to (\forall u \in A \forall v \in A (u = v \lor [u] R \cap [v] R = \emptyset) \leftrightarrow \forall x \exists^{*} u \in A u R x)$
13	10 12	bitr4id	$⊢ Rel R \to (Disj ({R ↾}_{A}) \leftrightarrow \forall u \in A \forall v \in A (u = v \lor [u] R \cap [v] R = \emptyset))$

Metamath Proof Explorer