reldisjun

Description: Split a relation into two disjoint parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023)

		Ref	Expression
	Assertion	reldisjun	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to R = ({R ↾}_{A}) \cup ({R ↾}_{B})$

Step	Hyp	Ref	Expression
1		reseq2	$⊢ dom R = A \cup B \to {R ↾}_{dom R} = {R ↾}_{(A \cup B)}$
2	1	3ad2ant2	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to {R ↾}_{dom R} = {R ↾}_{(A \cup B)}$
3		resdm	$⊢ Rel R \to {R ↾}_{dom R} = R$
4	3	3ad2ant1	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to {R ↾}_{dom R} = R$
5		resundi	$⊢ {R ↾}_{(A \cup B)} = ({R ↾}_{A}) \cup ({R ↾}_{B})$
6	5	a1i	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to {R ↾}_{(A \cup B)} = ({R ↾}_{A}) \cup ({R ↾}_{B})$
7	2 4 6	3eqtr3d	$⊢ (Rel R \land dom R = A \cup B \land A \cap B = \emptyset) \to R = ({R ↾}_{A}) \cup ({R ↾}_{B})$

Metamath Proof Explorer