Step |
Hyp |
Ref |
Expression |
1 |
|
setsval |
|- ( ( F e. V /\ Y e. U ) -> ( F sSet <. X , Y >. ) = ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ) |
2 |
1
|
3adant2 |
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( F sSet <. X , Y >. ) = ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ) |
3 |
2
|
fveq1d |
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = ( ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ` X ) ) |
4 |
|
simp2 |
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> X e. W ) |
5 |
|
simp3 |
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> Y e. U ) |
6 |
|
neldifsn |
|- -. X e. ( _V \ { X } ) |
7 |
|
dmres |
|- dom ( F |` ( _V \ { X } ) ) = ( ( _V \ { X } ) i^i dom F ) |
8 |
|
inss1 |
|- ( ( _V \ { X } ) i^i dom F ) C_ ( _V \ { X } ) |
9 |
7 8
|
eqsstri |
|- dom ( F |` ( _V \ { X } ) ) C_ ( _V \ { X } ) |
10 |
9
|
sseli |
|- ( X e. dom ( F |` ( _V \ { X } ) ) -> X e. ( _V \ { X } ) ) |
11 |
6 10
|
mto |
|- -. X e. dom ( F |` ( _V \ { X } ) ) |
12 |
11
|
a1i |
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> -. X e. dom ( F |` ( _V \ { X } ) ) ) |
13 |
|
fsnunfv |
|- ( ( X e. W /\ Y e. U /\ -. X e. dom ( F |` ( _V \ { X } ) ) ) -> ( ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ` X ) = Y ) |
14 |
4 5 12 13
|
syl3anc |
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ` X ) = Y ) |
15 |
3 14
|
eqtrd |
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = Y ) |