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

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 fvsnun2.4 
 |-  ( ph -> D e. ( C \ { A } ) )
5 3 reseq1i 
 |-  ( G |` ( C \ { A } ) ) = ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` ( C \ { A } ) )
6 5 a1i 
 |-  ( ph -> ( G |` ( C \ { A } ) ) = ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` ( C \ { A } ) ) )
7 resundir 
 |-  ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` ( C \ { A } ) ) = ( ( { <. A , B >. } |` ( C \ { A } ) ) u. ( ( F |` ( C \ { A } ) ) |` ( C \ { A } ) ) )
8 7 a1i 
 |-  ( ph -> ( ( { <. A , B >. } u. ( F |` ( C \ { A } ) ) ) |` ( C \ { A } ) ) = ( ( { <. A , B >. } |` ( C \ { A } ) ) u. ( ( F |` ( C \ { A } ) ) |` ( C \ { A } ) ) ) )
9 disjdif 
 |-  ( { A } i^i ( C \ { A } ) ) = (/)
10 fnsng 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. } Fn { A } )
11 1 2 10 syl2anc 
 |-  ( ph -> { <. A , B >. } Fn { A } )
12 fnresdisj 
 |-  ( { <. A , B >. } Fn { A } -> ( ( { A } i^i ( C \ { A } ) ) = (/) <-> ( { <. A , B >. } |` ( C \ { A } ) ) = (/) ) )
13 11 12 syl 
 |-  ( ph -> ( ( { A } i^i ( C \ { A } ) ) = (/) <-> ( { <. A , B >. } |` ( C \ { A } ) ) = (/) ) )
14 9 13 mpbii 
 |-  ( ph -> ( { <. A , B >. } |` ( C \ { A } ) ) = (/) )
15 residm 
 |-  ( ( F |` ( C \ { A } ) ) |` ( C \ { A } ) ) = ( F |` ( C \ { A } ) )
16 15 a1i 
 |-  ( ph -> ( ( F |` ( C \ { A } ) ) |` ( C \ { A } ) ) = ( F |` ( C \ { A } ) ) )
17 14 16 uneq12d 
 |-  ( ph -> ( ( { <. A , B >. } |` ( C \ { A } ) ) u. ( ( F |` ( C \ { A } ) ) |` ( C \ { A } ) ) ) = ( (/) u. ( F |` ( C \ { A } ) ) ) )
18 uncom 
 |-  ( (/) u. ( F |` ( C \ { A } ) ) ) = ( ( F |` ( C \ { A } ) ) u. (/) )
19 18 a1i 
 |-  ( ph -> ( (/) u. ( F |` ( C \ { A } ) ) ) = ( ( F |` ( C \ { A } ) ) u. (/) ) )
20 un0 
 |-  ( ( F |` ( C \ { A } ) ) u. (/) ) = ( F |` ( C \ { A } ) )
21 20 a1i 
 |-  ( ph -> ( ( F |` ( C \ { A } ) ) u. (/) ) = ( F |` ( C \ { A } ) ) )
22 17 19 21 3eqtrd 
 |-  ( ph -> ( ( { <. A , B >. } |` ( C \ { A } ) ) u. ( ( F |` ( C \ { A } ) ) |` ( C \ { A } ) ) ) = ( F |` ( C \ { A } ) ) )
23 6 8 22 3eqtrd 
 |-  ( ph -> ( G |` ( C \ { A } ) ) = ( F |` ( C \ { A } ) ) )
24 23 fveq1d 
 |-  ( ph -> ( ( G |` ( C \ { A } ) ) ` D ) = ( ( F |` ( C \ { A } ) ) ` D ) )
25 4 fvresd 
 |-  ( ph -> ( ( G |` ( C \ { A } ) ) ` D ) = ( G ` D ) )
26 4 fvresd 
 |-  ( ph -> ( ( F |` ( C \ { A } ) ) ` D ) = ( F ` D ) )
27 24 25 26 3eqtr3d 
 |-  ( ph -> ( G ` D ) = ( F ` D ) )