Metamath Proof Explorer


Theorem fvsnun1

Description: The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 . (Contributed by NM, 23-Sep-2007) Put in deduction form. (Revised by BJ, 25-Feb-2023)

Ref Expression
Hypotheses fvsnun.1 ( 𝜑𝐴𝑉 )
fvsnun.2 ( 𝜑𝐵𝑊 )
fvsnun.3 𝐺 = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
Assertion fvsnun1 ( 𝜑 → ( 𝐺𝐴 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 fvsnun.1 ( 𝜑𝐴𝑉 )
2 fvsnun.2 ( 𝜑𝐵𝑊 )
3 fvsnun.3 𝐺 = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
4 3 reseq1i ( 𝐺 ↾ { 𝐴 } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ { 𝐴 } )
5 resundir ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ { 𝐴 } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) )
6 disjdifr ( ( 𝐶 ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅
7 resdisj ( ( ( 𝐶 ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅ → ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) = ∅ )
8 6 7 ax-mp ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) = ∅
9 8 uneq2i ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ∅ )
10 un0 ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ∅ ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
11 9 10 eqtri ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ { 𝐴 } ) ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
12 5 11 eqtri ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ { 𝐴 } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
13 4 12 eqtri ( 𝐺 ↾ { 𝐴 } ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } )
14 13 fveq1i ( ( 𝐺 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 )
15 snidg ( 𝐴𝑉𝐴 ∈ { 𝐴 } )
16 1 15 syl ( 𝜑𝐴 ∈ { 𝐴 } )
17 16 fvresd ( 𝜑 → ( ( 𝐺 ↾ { 𝐴 } ) ‘ 𝐴 ) = ( 𝐺𝐴 ) )
18 16 fvresd ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) )
19 fvsng ( ( 𝐴𝑉𝐵𝑊 ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )
20 1 2 19 syl2anc ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )
21 18 20 eqtrd ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ { 𝐴 } ) ‘ 𝐴 ) = 𝐵 )
22 14 17 21 3eqtr3a ( 𝜑 → ( 𝐺𝐴 ) = 𝐵 )