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