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	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) = ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		mptun	⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) = ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) )
2		inundif	⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
3		eqid	⊢ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) = if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 )
4	2 3	mpteq12i	⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) )
5		elinel2	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ 𝐵 )
6	5	iftrued	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) → if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) = 𝐶 )
7	6	mpteq2ia	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 )
8		eldifn	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ 𝑥 ∈ 𝐵 )
9	8	iffalsed	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) = 𝐷 )
10	9	mpteq2ia	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) = ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝐷 )
11	7 10	uneq12i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) ) = ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝐷 ) )
12	1 4 11	3eqtr3i	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝐷 ) ) = ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ 𝐶 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↦ 𝐷 ) )