Metamath Proof Explorer

Theorem suppss3

Description: Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses suppss3.1 
|- G = ( x e. A |-> B )
suppss3.a 
|- ( ph -> A e. V )
suppss3.z 
|- ( ph -> Z e. W )
suppss3.2 
|- ( ph -> F Fn A )
suppss3.3 
|- ( ( ph /\ x e. A /\ ( F ` x ) = Z ) -> B = Z )
Assertion suppss3 
|- ( ph -> ( G supp Z ) C_ ( F supp Z ) )

Proof

Step Hyp Ref Expression
1 suppss3.1 
 |-  G = ( x e. A |-> B )
2 suppss3.a 
 |-  ( ph -> A e. V )
3 suppss3.z 
 |-  ( ph -> Z e. W )
4 suppss3.2 
 |-  ( ph -> F Fn A )
5 suppss3.3 
 |-  ( ( ph /\ x e. A /\ ( F ` x ) = Z ) -> B = Z )
6 1 oveq1i 
 |-  ( G supp Z ) = ( ( x e. A |-> B ) supp Z )
7 simpl 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> ph )
8 eldifi 
 |-  ( x e. ( A \ ( F supp Z ) ) -> x e. A )
9 8 adantl 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> x e. A )
10 fnex 
 |-  ( ( F Fn A /\ A e. V ) -> F e. _V )
11 4 2 10 syl2anc 
 |-  ( ph -> F e. _V )
12 suppimacnv 
 |-  ( ( F e. _V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
13 11 3 12 syl2anc 
 |-  ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
14 13 eleq2d 
 |-  ( ph -> ( x e. ( F supp Z ) <-> x e. ( `' F " ( _V \ { Z } ) ) ) )
15 elpreima 
 |-  ( F Fn A -> ( x e. ( `' F " ( _V \ { Z } ) ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { Z } ) ) ) )
16 4 15 syl 
 |-  ( ph -> ( x e. ( `' F " ( _V \ { Z } ) ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { Z } ) ) ) )
17 14 16 bitrd 
 |-  ( ph -> ( x e. ( F supp Z ) <-> ( x e. A /\ ( F ` x ) e. ( _V \ { Z } ) ) ) )
18 17 baibd 
 |-  ( ( ph /\ x e. A ) -> ( x e. ( F supp Z ) <-> ( F ` x ) e. ( _V \ { Z } ) ) )
19 18 notbid 
 |-  ( ( ph /\ x e. A ) -> ( -. x e. ( F supp Z ) <-> -. ( F ` x ) e. ( _V \ { Z } ) ) )
20 19 biimpd 
 |-  ( ( ph /\ x e. A ) -> ( -. x e. ( F supp Z ) -> -. ( F ` x ) e. ( _V \ { Z } ) ) )
21 20 expimpd 
 |-  ( ph -> ( ( x e. A /\ -. x e. ( F supp Z ) ) -> -. ( F ` x ) e. ( _V \ { Z } ) ) )
22 eldif 
 |-  ( x e. ( A \ ( F supp Z ) ) <-> ( x e. A /\ -. x e. ( F supp Z ) ) )
23 fvex 
 |-  ( F ` x ) e. _V
24 eldifsn 
 |-  ( ( F ` x ) e. ( _V \ { Z } ) <-> ( ( F ` x ) e. _V /\ ( F ` x ) =/= Z ) )
25 23 24 mpbiran 
 |-  ( ( F ` x ) e. ( _V \ { Z } ) <-> ( F ` x ) =/= Z )
26 25 necon2bbii 
 |-  ( ( F ` x ) = Z <-> -. ( F ` x ) e. ( _V \ { Z } ) )
27 21 22 26 3imtr4g 
 |-  ( ph -> ( x e. ( A \ ( F supp Z ) ) -> ( F ` x ) = Z ) )
28 27 imp 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> ( F ` x ) = Z )
29 7 9 28 5 syl3anc 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> B = Z )
30 29 2 suppss2 
 |-  ( ph -> ( ( x e. A |-> B ) supp Z ) C_ ( F supp Z ) )
31 6 30 eqsstrid 
 |-  ( ph -> ( G supp Z ) C_ ( F supp Z ) )