Metamath Proof Explorer

Theorem fmptunsnop

Description: Two ways to express a function with a value replaced. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses fmptunsnop.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
fmptunsnop.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
fmptunsnop.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion fmptunsnop ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 fmptunsnop.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 fmptunsnop.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3 fmptunsnop.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4 mptun ⊢ ( 𝑥 ∈ ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) ∪ ( 𝑥 ∈ { 𝑋 } ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) )
5 difsnid ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝐴 )
6 2 5 syl ⊢ ( 𝜑 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝐴 )
7 6 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) )
8 eldifsni ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) → 𝑥 ≠ 𝑋 )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ) → 𝑥 ≠ 𝑋 )
10 9 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ) → ¬ 𝑥 = 𝑋 )
11 10 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ) → if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
12 11 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
13 dffn3 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
14 1 13 sylib ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
15 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑋 } ) ⊆ 𝐴 )
16 14 15 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
17 12 16 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) )
18 iftrue ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) = 𝑌 )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) = 𝑌 )
20 19 2 3 fmptsnd ⊢ ( 𝜑 → { ⟨ 𝑋 , 𝑌 ⟩ } = ( 𝑥 ∈ { 𝑋 } ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) )
21 20 eqcomd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑋 } ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) = { ⟨ 𝑋 , 𝑌 ⟩ } )
22 17 21 uneq12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) ∪ ( 𝑥 ∈ { 𝑋 } ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
23 4 7 22 3eqtr3a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 = 𝑋 , 𝑌 , ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )