relresdm1

Description: Restriction of a disjoint union to the domain of the first term. (Contributed by Thierry Arnoux, 9-Dec-2021)

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

Step	Hyp	Ref	Expression
1		resundir	$⊢ {(A \cup B) ↾}_{dom A} = ({A ↾}_{dom A}) \cup ({B ↾}_{dom A})$
2		resdm	$⊢ Rel A \to {A ↾}_{dom A} = A$
3	2	adantr	$⊢ (Rel A \land dom A \cap dom B = \emptyset) \to {A ↾}_{dom A} = A$
4		dmres	$⊢ dom ({B ↾}_{dom A}) = dom A \cap dom B$
5		simpr	$⊢ (Rel A \land dom A \cap dom B = \emptyset) \to dom A \cap dom B = \emptyset$
6	4 5	eqtrid	$⊢ (Rel A \land dom A \cap dom B = \emptyset) \to dom ({B ↾}_{dom A}) = \emptyset$
7		relres	$⊢ Rel ({B ↾}_{dom A})$
8		reldm0	$⊢ Rel ({B ↾}_{dom A}) \to ({B ↾}_{dom A} = \emptyset \leftrightarrow dom ({B ↾}_{dom A}) = \emptyset)$
9	7 8	ax-mp	$⊢ {B ↾}_{dom A} = \emptyset \leftrightarrow dom ({B ↾}_{dom A}) = \emptyset$
10	6 9	sylibr	$⊢ (Rel A \land dom A \cap dom B = \emptyset) \to {B ↾}_{dom A} = \emptyset$
11	3 10	uneq12d	$⊢ (Rel A \land dom A \cap dom B = \emptyset) \to ({A ↾}_{dom A}) \cup ({B ↾}_{dom A}) = A \cup \emptyset$
12		un0	$⊢ A \cup \emptyset = A$
13	11 12	eqtrdi	$⊢ (Rel A \land dom A \cap dom B = \emptyset) \to ({A ↾}_{dom A}) \cup ({B ↾}_{dom A}) = A$
14	1 13	eqtrid	$⊢ (Rel A \land dom A \cap dom B = \emptyset) \to {(A \cup B) ↾}_{dom A} = A$

Metamath Proof Explorer