fnunres2

Description: Restriction of a disjoint union to the domain of the second function. (Contributed by Thierry Arnoux, 12-Oct-2023)

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

Step	Hyp	Ref	Expression
1		uncom	$⊢ F \cup G = G \cup F$
2	1	reseq1i	$⊢ {(F \cup G) ↾}_{B} = {(G \cup F) ↾}_{B}$
3		simp2	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to G Fn B$
4		simp1	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to F Fn A$
5		incom	$⊢ A \cap B = B \cap A$
6		simp3	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to A \cap B = \emptyset$
7	5 6	eqtr3id	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to B \cap A = \emptyset$
8		fnunres1	$⊢ (G Fn B \land F Fn A \land B \cap A = \emptyset) \to {(G \cup F) ↾}_{B} = G$
9	3 4 7 8	syl3anc	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(G \cup F) ↾}_{B} = G$
10	2 9	syl5eq	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(F \cup G) ↾}_{B} = G$

Metamath Proof Explorer