This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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