Step |
Hyp |
Ref |
Expression |
1 |
|
difss |
|- ( A \ { X } ) C_ A |
2 |
|
fssres |
|- ( ( F : A --> B /\ ( A \ { X } ) C_ A ) -> ( F |` ( A \ { X } ) ) : ( A \ { X } ) --> B ) |
3 |
1 2
|
mpan2 |
|- ( F : A --> B -> ( F |` ( A \ { X } ) ) : ( A \ { X } ) --> B ) |
4 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
5 |
|
fnresdm |
|- ( F Fn A -> ( F |` A ) = F ) |
6 |
4 5
|
syl |
|- ( F : A --> B -> ( F |` A ) = F ) |
7 |
6
|
reseq1d |
|- ( F : A --> B -> ( ( F |` A ) |` ( _V \ { X } ) ) = ( F |` ( _V \ { X } ) ) ) |
8 |
|
resres |
|- ( ( F |` A ) |` ( _V \ { X } ) ) = ( F |` ( A i^i ( _V \ { X } ) ) ) |
9 |
|
invdif |
|- ( A i^i ( _V \ { X } ) ) = ( A \ { X } ) |
10 |
9
|
reseq2i |
|- ( F |` ( A i^i ( _V \ { X } ) ) ) = ( F |` ( A \ { X } ) ) |
11 |
8 10
|
eqtri |
|- ( ( F |` A ) |` ( _V \ { X } ) ) = ( F |` ( A \ { X } ) ) |
12 |
7 11
|
eqtr3di |
|- ( F : A --> B -> ( F |` ( _V \ { X } ) ) = ( F |` ( A \ { X } ) ) ) |
13 |
12
|
feq1d |
|- ( F : A --> B -> ( ( F |` ( _V \ { X } ) ) : ( A \ { X } ) --> B <-> ( F |` ( A \ { X } ) ) : ( A \ { X } ) --> B ) ) |
14 |
3 13
|
mpbird |
|- ( F : A --> B -> ( F |` ( _V \ { X } ) ) : ( A \ { X } ) --> B ) |
15 |
14
|
adantl |
|- ( ( F e. V /\ F : A --> B ) -> ( F |` ( _V \ { X } ) ) : ( A \ { X } ) --> B ) |
16 |
|
fsnunf2 |
|- ( ( ( F |` ( _V \ { X } ) ) : ( A \ { X } ) --> B /\ X e. A /\ Y e. B ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) : A --> B ) |
17 |
15 16
|
syl3an1 |
|- ( ( ( F e. V /\ F : A --> B ) /\ X e. A /\ Y e. B ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) : A --> B ) |
18 |
|
simp1l |
|- ( ( ( F e. V /\ F : A --> B ) /\ X e. A /\ Y e. B ) -> F e. V ) |
19 |
|
simp3 |
|- ( ( ( F e. V /\ F : A --> B ) /\ X e. A /\ Y e. B ) -> Y e. B ) |
20 |
|
setsval |
|- ( ( F e. V /\ Y e. B ) -> ( F sSet <. X , Y >. ) = ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) ) |
21 |
20
|
feq1d |
|- ( ( F e. V /\ Y e. B ) -> ( ( F sSet <. X , Y >. ) : A --> B <-> ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) : A --> B ) ) |
22 |
18 19 21
|
syl2anc |
|- ( ( ( F e. V /\ F : A --> B ) /\ X e. A /\ Y e. B ) -> ( ( F sSet <. X , Y >. ) : A --> B <-> ( ( F |` ( _V \ { X } ) ) u. { <. X , Y >. } ) : A --> B ) ) |
23 |
17 22
|
mpbird |
|- ( ( ( F e. V /\ F : A --> B ) /\ X e. A /\ Y e. B ) -> ( F sSet <. X , Y >. ) : A --> B ) |