Theorem partfun 6716

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.)

Assertion

Ref	Expression
partfun	⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ 𝐷))

Proof of Theorem partfun

Step	Hyp	Ref	Expression
1		mptun 6715	. 2 ⊢ (𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)))
2		inundif 4485	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴
3		eqid 2735	. . 3 ⊢ if(𝑥 ∈ 𝐵, 𝐶, 𝐷) = if(𝑥 ∈ 𝐵, 𝐶, 𝐷)
4	2, 3	mpteq12i 5254	. 2 ⊢ (𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷))
5		elinel2 4212	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐵)
6	5	iftrued 4539	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → if(𝑥 ∈ 𝐵, 𝐶, 𝐷) = 𝐶)
7	6	mpteq2ia 5251	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶)
8		eldifn 4142	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
9	8	iffalsed 4542	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → if(𝑥 ∈ 𝐵, 𝐶, 𝐷) = 𝐷)
10	9	mpteq2ia 5251	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ 𝐷)
11	7, 10	uneq12i 4176	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷))) = ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ 𝐷))
12	1, 4, 11	3eqtr3i 2771	1 ⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ 𝐷))

Syntax hints:   = wceq 1537   ∈ wcel 2106   ∖ cdif 3960   ∪ cun 3961   ∩ cin 3962  ifcif 4531   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-if 4532  df-opab 5211  df-mpt 5232

This theorem is referenced by:  mptiffisupp  32708  mptprop  32713  cycpm2tr  33122  redvmptabs  42369  fsuppssindlem2  42579