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 
|- ( 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 )