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

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 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 𝐵 )