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		ineqcom	$⊢ A \cap B = \emptyset \leftrightarrow B \cap A = \emptyset$
4		fnunres1	$⊢ (G Fn B \land F Fn A \land B \cap A = \emptyset) \to {(G \cup F) ↾}_{B} = G$
5	3 4	syl3an3b	$⊢ (G Fn B \land F Fn A \land A \cap B = \emptyset) \to {(G \cup F) ↾}_{B} = G$
6	5	3com12	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(G \cup F) ↾}_{B} = G$
7	2 6	eqtrid	$⊢ (F Fn A \land G Fn B \land A \cap B = \emptyset) \to {(F \cup G) ↾}_{B} = G$

Metamath Proof Explorer