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 
|- ( x e. A |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) )

Proof

Step Hyp Ref Expression
1 mptun 
 |-  ( x e. ( ( A i^i B ) u. ( A \ B ) ) |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) u. ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) )
2 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
3 eqid 
 |-  if ( x e. B , C , D ) = if ( x e. B , C , D )
4 2 3 mpteq12i 
 |-  ( x e. ( ( A i^i B ) u. ( A \ B ) ) |-> if ( x e. B , C , D ) ) = ( x e. A |-> if ( x e. B , C , D ) )
5 elinel2 
 |-  ( x e. ( A i^i B ) -> x e. B )
6 5 iftrued 
 |-  ( x e. ( A i^i B ) -> if ( x e. B , C , D ) = C )
7 6 mpteq2ia 
 |-  ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) = ( x e. ( A i^i B ) |-> C )
8 eldifn 
 |-  ( x e. ( A \ B ) -> -. x e. B )
9 8 iffalsed 
 |-  ( x e. ( A \ B ) -> if ( x e. B , C , D ) = D )
10 9 mpteq2ia 
 |-  ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) = ( x e. ( A \ B ) |-> D )
11 7 10 uneq12i 
 |-  ( ( x e. ( A i^i B ) |-> if ( x e. B , C , D ) ) u. ( x e. ( A \ B ) |-> if ( x e. B , C , D ) ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) )
12 1 4 11 3eqtr3i 
 |-  ( x e. A |-> if ( x e. B , C , D ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> D ) )