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

Metamath Proof Explorer

Theorem partfun2

Description: Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. See also partfun and ifmpt2v . (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypothesis partfun2.1 
|- D = { x e. A | ph }
Assertion partfun2 
|- ( x e. A |-> if ( ph , B , C ) ) = ( ( x e. D |-> B ) u. ( x e. ( A \ D ) |-> C ) )

Proof

Step Hyp Ref Expression
1 partfun2.1 
 |-  D = { x e. A | ph }
2 partfun 
 |-  ( x e. A |-> if ( x e. D , B , C ) ) = ( ( x e. ( A i^i D ) |-> B ) u. ( x e. ( A \ D ) |-> C ) )
3 1 reqabi 
 |-  ( x e. D <-> ( x e. A /\ ph ) )
4 3 baib 
 |-  ( x e. A -> ( x e. D <-> ph ) )
5 4 ifbid 
 |-  ( x e. A -> if ( x e. D , B , C ) = if ( ph , B , C ) )
6 5 mpteq2ia 
 |-  ( x e. A |-> if ( x e. D , B , C ) ) = ( x e. A |-> if ( ph , B , C ) )
7 1 ssrab3 
 |-  D C_ A
8 sseqin2 
 |-  ( D C_ A <-> ( A i^i D ) = D )
9 7 8 mpbi 
 |-  ( A i^i D ) = D
10 9 mpteq1i 
 |-  ( x e. ( A i^i D ) |-> B ) = ( x e. D |-> B )
11 10 uneq1i 
 |-  ( ( x e. ( A i^i D ) |-> B ) u. ( x e. ( A \ D ) |-> C ) ) = ( ( x e. D |-> B ) u. ( x e. ( A \ D ) |-> C ) )
12 2 6 11 3eqtr3i 
 |-  ( x e. A |-> if ( ph , B , C ) ) = ( ( x e. D |-> B ) u. ( x e. ( A \ D ) |-> C ) )