Metamath Proof Explorer

Theorem fvsnun2

Description: The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 . (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 ⊢ 𝐺 = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
fvsnun2.4 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ∖ { 𝐴 } ) )
Assertion fvsnun2 ( 𝜑 → ( 𝐺 ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fvsnun.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 fvsnun.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 fvsnun.3 ⊢ 𝐺 = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
4 fvsnun2.4 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ∖ { 𝐴 } ) )
5 3 reseq1i ⊢ ( 𝐺 ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) )
6 5 a1i ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
7 resundir ⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
8 7 a1i ⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) )
9 disjdif ⊢ ( { 𝐴 } ∩ ( 𝐶 ∖ { 𝐴 } ) ) = ∅
10 fnsng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } )
11 1 2 10 syl2anc ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } )
12 fnresdisj ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } → ( ( { 𝐴 } ∩ ( 𝐶 ∖ { 𝐴 } ) ) = ∅ ↔ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ∅ ) )
13 11 12 syl ⊢ ( 𝜑 → ( ( { 𝐴 } ∩ ( 𝐶 ∖ { 𝐴 } ) ) = ∅ ↔ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ∅ ) )
14 9 13 mpbii ⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ∅ )
15 residm ⊢ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) )
16 15 a1i ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
17 14 16 uneq12d ⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) = ( ∅ ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) )
18 uncom ⊢ ( ∅ ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ∅ )
19 18 a1i ⊢ ( 𝜑 → ( ∅ ∪ ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ∅ ) )
20 un0 ⊢ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ∅ ) = ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) )
21 20 a1i ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ∅ ) = ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
22 17 19 21 3eqtrd ⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ ( 𝐶 ∖ { 𝐴 } ) ) ∪ ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ↾ ( 𝐶 ∖ { 𝐴 } ) ) ) = ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
23 6 8 22 3eqtrd ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝐶 ∖ { 𝐴 } ) ) = ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) )
24 23 fveq1d ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ‘ 𝐷 ) = ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ‘ 𝐷 ) )
25 4 fvresd ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ‘ 𝐷 ) = ( 𝐺 ‘ 𝐷 ) )
26 4 fvresd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐶 ∖ { 𝐴 } ) ) ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) )
27 24 25 26 3eqtr3d ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) )