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	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
	Assertion	partfun2	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		partfun2.1	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
2		partfun	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐷 , 𝐵 , 𝐶 ) ) = ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) )
3	1	reqabi	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
4	3	baib	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐷 ↔ 𝜑 ) )
5	4	ifbid	⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐷 , 𝐵 , 𝐶 ) = if ( 𝜑 , 𝐵 , 𝐶 ) )
6	5	mpteq2ia	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐷 , 𝐵 , 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) )
7	1	ssrab3	⊢ 𝐷 ⊆ 𝐴
8		sseqin2	⊢ ( 𝐷 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐷 ) = 𝐷 )
9	7 8	mpbi	⊢ ( 𝐴 ∩ 𝐷 ) = 𝐷
10	9	mpteq1i	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
11	10	uneq1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐵 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) )
12	2 6 11	3eqtr3i	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ∪ ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) )