fnunres1

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

		Ref	Expression
	Assertion	fnunres1	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(F \cup G) ↾}_{A} = F$

Step	Hyp	Ref	Expression
1		fndm	$⊢ F Fn A \to dom F = A$
2	1	3ad2ant1	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to dom F = A$
3	2	reseq2d	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(F \cup G) ↾}_{dom F} = {(F \cup G) ↾}_{A}$
4		fnrel	$⊢ F Fn A \to Rel F$
5	4	3ad2ant1	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to Rel F$
6		fndm	$⊢ G Fn B \to dom G = B$
7	6	3ad2ant2	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to dom G = B$
8	2 7	ineq12d	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to dom F \cap dom G = A \cap B$
9		simp3	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to A \cap B = \emptyset$
10	8 9	eqtrd	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to dom F \cap dom G = \emptyset$
11		funresdm1	$⊢ (Rel F \land dom F \cap dom G = \emptyset) \to {(F \cup G) ↾}_{dom F} = F$
12	5 10 11	syl2anc	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(F \cup G) ↾}_{dom F} = F$
13	3 12	eqtr3d	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(F \cup G) ↾}_{A} = F$

Metamath Proof Explorer