Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( X e. V /\ Y e. W ) ) |
2 |
1
|
anim2i |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> ( Z e. _V /\ ( X e. V /\ Y e. W ) ) ) |
3 |
2
|
ancomd |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> ( ( X e. V /\ Y e. W ) /\ Z e. _V ) ) |
4 |
|
df-3an |
|- ( ( X e. V /\ Y e. W /\ Z e. _V ) <-> ( ( X e. V /\ Y e. W ) /\ Z e. _V ) ) |
5 |
3 4
|
sylibr |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> ( X e. V /\ Y e. W /\ Z e. _V ) ) |
6 |
|
snopfsupp |
|- ( ( X e. V /\ Y e. W /\ Z e. _V ) -> { <. X , Y >. } finSupp Z ) |
7 |
5 6
|
syl |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> { <. X , Y >. } finSupp Z ) |
8 |
|
funsng |
|- ( ( X e. V /\ Y e. W ) -> Fun { <. X , Y >. } ) |
9 |
|
simpl |
|- ( ( Fun F /\ X e/ dom F ) -> Fun F ) |
10 |
8 9
|
anim12ci |
|- ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( Fun F /\ Fun { <. X , Y >. } ) ) |
11 |
|
dmsnopg |
|- ( Y e. W -> dom { <. X , Y >. } = { X } ) |
12 |
11
|
adantl |
|- ( ( X e. V /\ Y e. W ) -> dom { <. X , Y >. } = { X } ) |
13 |
12
|
ineq2d |
|- ( ( X e. V /\ Y e. W ) -> ( dom F i^i dom { <. X , Y >. } ) = ( dom F i^i { X } ) ) |
14 |
|
df-nel |
|- ( X e/ dom F <-> -. X e. dom F ) |
15 |
|
disjsn |
|- ( ( dom F i^i { X } ) = (/) <-> -. X e. dom F ) |
16 |
14 15
|
sylbb2 |
|- ( X e/ dom F -> ( dom F i^i { X } ) = (/) ) |
17 |
16
|
adantl |
|- ( ( Fun F /\ X e/ dom F ) -> ( dom F i^i { X } ) = (/) ) |
18 |
13 17
|
sylan9eq |
|- ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( dom F i^i dom { <. X , Y >. } ) = (/) ) |
19 |
10 18
|
jca |
|- ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( ( Fun F /\ Fun { <. X , Y >. } ) /\ ( dom F i^i dom { <. X , Y >. } ) = (/) ) ) |
20 |
19
|
adantl |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> ( ( Fun F /\ Fun { <. X , Y >. } ) /\ ( dom F i^i dom { <. X , Y >. } ) = (/) ) ) |
21 |
|
funun |
|- ( ( ( Fun F /\ Fun { <. X , Y >. } ) /\ ( dom F i^i dom { <. X , Y >. } ) = (/) ) -> Fun ( F u. { <. X , Y >. } ) ) |
22 |
20 21
|
syl |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> Fun ( F u. { <. X , Y >. } ) ) |
23 |
22
|
fsuppunbi |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> ( ( F u. { <. X , Y >. } ) finSupp Z <-> ( F finSupp Z /\ { <. X , Y >. } finSupp Z ) ) ) |
24 |
7 23
|
mpbiran2d |
|- ( ( Z e. _V /\ ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) ) -> ( ( F u. { <. X , Y >. } ) finSupp Z <-> F finSupp Z ) ) |
25 |
24
|
ex |
|- ( Z e. _V -> ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( ( F u. { <. X , Y >. } ) finSupp Z <-> F finSupp Z ) ) ) |
26 |
|
relfsupp |
|- Rel finSupp |
27 |
26
|
brrelex2i |
|- ( ( F u. { <. X , Y >. } ) finSupp Z -> Z e. _V ) |
28 |
26
|
brrelex2i |
|- ( F finSupp Z -> Z e. _V ) |
29 |
27 28
|
pm5.21ni |
|- ( -. Z e. _V -> ( ( F u. { <. X , Y >. } ) finSupp Z <-> F finSupp Z ) ) |
30 |
29
|
a1d |
|- ( -. Z e. _V -> ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( ( F u. { <. X , Y >. } ) finSupp Z <-> F finSupp Z ) ) ) |
31 |
25 30
|
pm2.61i |
|- ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( ( F u. { <. X , Y >. } ) finSupp Z <-> F finSupp Z ) ) |