Metamath Proof Explorer

Theorem suppiniseg

Description: Relation between the support ( F supp Z ) and the initial segment (`' F " { Z } ) ` . (Contributed by Thierry Arnoux, 25-Jun-2024)

Ref Expression
Assertion suppiniseg 
|- ( ( Fun F /\ F e. V /\ Z e. W ) -> ( dom F \ ( F supp Z ) ) = ( `' F " { Z } ) )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( x e. ( dom F \ ( F supp Z ) ) <-> ( x e. dom F /\ -. x e. ( F supp Z ) ) )
2 funfn 
 |-  ( Fun F <-> F Fn dom F )
3 2 biimpi 
 |-  ( Fun F -> F Fn dom F )
4 elsuppfng 
 |-  ( ( F Fn dom F /\ F e. V /\ Z e. W ) -> ( x e. ( F supp Z ) <-> ( x e. dom F /\ ( F ` x ) =/= Z ) ) )
5 3 4 syl3an1 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( x e. ( F supp Z ) <-> ( x e. dom F /\ ( F ` x ) =/= Z ) ) )
6 5 baibd 
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( x e. ( F supp Z ) <-> ( F ` x ) =/= Z ) )
7 6 notbid 
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( -. x e. ( F supp Z ) <-> -. ( F ` x ) =/= Z ) )
8 nne 
 |-  ( -. ( F ` x ) =/= Z <-> ( F ` x ) = Z )
9 7 8 bitrdi 
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( -. x e. ( F supp Z ) <-> ( F ` x ) = Z ) )
10 fvex 
 |-  ( F ` x ) e. _V
11 10 elsn 
 |-  ( ( F ` x ) e. { Z } <-> ( F ` x ) = Z )
12 9 11 bitr4di 
 |-  ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( -. x e. ( F supp Z ) <-> ( F ` x ) e. { Z } ) )
13 12 pm5.32da 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( ( x e. dom F /\ -. x e. ( F supp Z ) ) <-> ( x e. dom F /\ ( F ` x ) e. { Z } ) ) )
14 1 13 bitrid 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( x e. ( dom F \ ( F supp Z ) ) <-> ( x e. dom F /\ ( F ` x ) e. { Z } ) ) )
15 3 3ad2ant1 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> F Fn dom F )
16 elpreima 
 |-  ( F Fn dom F -> ( x e. ( `' F " { Z } ) <-> ( x e. dom F /\ ( F ` x ) e. { Z } ) ) )
17 15 16 syl 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( x e. ( `' F " { Z } ) <-> ( x e. dom F /\ ( F ` x ) e. { Z } ) ) )
18 14 17 bitr4d 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( x e. ( dom F \ ( F supp Z ) ) <-> x e. ( `' F " { Z } ) ) )
19 18 eqrdv 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( dom F \ ( F supp Z ) ) = ( `' F " { Z } ) )