Metamath Proof Explorer

Theorem partfun

Description: Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. (Contributed by Thierry Arnoux, 30-Mar-2017)

		Ref	Expression
	Assertion	partfun	$⊢ (x \in A ⟼ if (x \in B, C, D)) = (x \in (A \cap B) ⟼ C) \cup (x \in (A ∖ B) ⟼ D)$

Proof

Step	Hyp	Ref	Expression
1		mptun	$⊢ (x \in ((A \cap B) \cup (A ∖ B)) ⟼ if (x \in B, C, D)) = (x \in (A \cap B) ⟼ if (x \in B, C, D)) \cup (x \in (A ∖ B) ⟼ if (x \in B, C, D))$
2		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
3		eqid	$⊢ if (x \in B, C, D) = if (x \in B, C, D)$
4	2 3	mpteq12i	$⊢ (x \in ((A \cap B) \cup (A ∖ B)) ⟼ if (x \in B, C, D)) = (x \in A ⟼ if (x \in B, C, D))$
5		elinel2	$⊢ x \in (A \cap B) \to x \in B$
6	5	iftrued	$⊢ x \in (A \cap B) \to if (x \in B, C, D) = C$
7	6	mpteq2ia	$⊢ (x \in (A \cap B) ⟼ if (x \in B, C, D)) = (x \in (A \cap B) ⟼ C)$
8		eldifn	$⊢ x \in (A ∖ B) \to \neg x \in B$
9	8	iffalsed	$⊢ x \in (A ∖ B) \to if (x \in B, C, D) = D$
10	9	mpteq2ia	$⊢ (x \in (A ∖ B) ⟼ if (x \in B, C, D)) = (x \in (A ∖ B) ⟼ D)$
11	7 10	uneq12i	$⊢ (x \in (A \cap B) ⟼ if (x \in B, C, D)) \cup (x \in (A ∖ B) ⟼ if (x \in B, C, D)) = (x \in (A \cap B) ⟼ C) \cup (x \in (A ∖ B) ⟼ D)$
12	1 4 11	3eqtr3i	$⊢ (x \in A ⟼ if (x \in B, C, D)) = (x \in (A \cap B) ⟼ C) \cup (x \in (A ∖ B) ⟼ D)$