Metamath Proof Explorer


Theorem funsnfsupp

Description: Finite support for a function extended by a singleton. (Contributed by Stefan O'Rear, 27-Feb-2015) (Revised by AV, 19-Jul-2019)

Ref Expression
Assertion funsnfsupp
|- ( ( ( X e. V /\ Y e. W ) /\ ( Fun F /\ X e/ dom F ) ) -> ( ( F u. { <. X , Y >. } ) finSupp Z <-> F finSupp Z ) )

Proof

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