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
|- ( ph -> A e. V )
fvsnun.2
|- ( ph -> B e. W )
fvsnun.3
|- G = ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) )
Assertion fvsnun1
|- ( ph -> ( G ` A ) = B )

Proof

Step Hyp Ref Expression
1 fvsnun.1
 |-  ( ph -> A e. V )
2 fvsnun.2
 |-  ( ph -> B e. W )
3 fvsnun.3
 |-  G = ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) )
4 3 reseq1i
 |-  ( G |` { A } ) = ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` { A } )
5 resundir
 |-  ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` { A } ) = ( ( { <. A , B >. } |` { A } ) u. ( ( F |` ( C \ { A } ) ) |` { A } ) )
6 disjdifr
 |-  ( ( C \ { A } ) i^i { A } ) = (/)
7 resdisj
 |-  ( ( ( C \ { A } ) i^i { A } ) = (/) -> ( ( F |` ( C \ { A } ) ) |` { A } ) = (/) )
8 6 7 ax-mp
 |-  ( ( F |` ( C \ { A } ) ) |` { A } ) = (/)
9 8 uneq2i
 |-  ( ( { <. A , B >. } |` { A } ) u. ( ( F |` ( C \ { A } ) ) |` { A } ) ) = ( ( { <. A , B >. } |` { A } ) u. (/) )
10 un0
 |-  ( ( { <. A , B >. } |` { A } ) u. (/) ) = ( { <. A , B >. } |` { A } )
11 9 10 eqtri
 |-  ( ( { <. A , B >. } |` { A } ) u. ( ( F |` ( C \ { A } ) ) |` { A } ) ) = ( { <. A , B >. } |` { A } )
12 5 11 eqtri
 |-  ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` { A } ) = ( { <. A , B >. } |` { A } )
13 4 12 eqtri
 |-  ( G |` { A } ) = ( { <. A , B >. } |` { A } )
14 13 fveq1i
 |-  ( ( G |` { A } ) ` A ) = ( ( { <. A , B >. } |` { A } ) ` A )
15 snidg
 |-  ( A e. V -> A e. { A } )
16 1 15 syl
 |-  ( ph -> A e. { A } )
17 16 fvresd
 |-  ( ph -> ( ( G |` { A } ) ` A ) = ( G ` A ) )
18 16 fvresd
 |-  ( ph -> ( ( { <. A , B >. } |` { A } ) ` A ) = ( { <. A , B >. } ` A ) )
19 fvsng
 |-  ( ( A e. V /\ B e. W ) -> ( { <. A , B >. } ` A ) = B )
20 1 2 19 syl2anc
 |-  ( ph -> ( { <. A , B >. } ` A ) = B )
21 18 20 eqtrd
 |-  ( ph -> ( ( { <. A , B >. } |` { A } ) ` A ) = B )
22 14 17 21 3eqtr3a
 |-  ( ph -> ( G ` A ) = B )