Metamath Proof Explorer

Theorem suppfnss

Description: The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 6-Jun-2022)

Ref Expression
Assertion suppfnss 
|- ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) -> ( F supp Z ) C_ ( G supp Z ) ) )

Proof

Step Hyp Ref Expression
1 simpr1 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> A C_ B )
2 fndm 
 |-  ( F Fn A -> dom F = A )
3 2 ad2antrr 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> dom F = A )
4 fndm 
 |-  ( G Fn B -> dom G = B )
5 4 ad2antlr 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> dom G = B )
6 1 3 5 3sstr4d 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> dom F C_ dom G )
7 6 adantr 
 |-  ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) -> dom F C_ dom G )
8 2 eleq2d 
 |-  ( F Fn A -> ( y e. dom F <-> y e. A ) )
9 8 ad2antrr 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( y e. dom F <-> y e. A ) )
10 fveqeq2 
 |-  ( x = y -> ( ( G ` x ) = Z <-> ( G ` y ) = Z ) )
11 fveqeq2 
 |-  ( x = y -> ( ( F ` x ) = Z <-> ( F ` y ) = Z ) )
12 10 11 imbi12d 
 |-  ( x = y -> ( ( ( G ` x ) = Z -> ( F ` x ) = Z ) <-> ( ( G ` y ) = Z -> ( F ` y ) = Z ) ) )
13 12 rspcv 
 |-  ( y e. A -> ( A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) -> ( ( G ` y ) = Z -> ( F ` y ) = Z ) ) )
14 9 13 syl6bi 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( y e. dom F -> ( A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) -> ( ( G ` y ) = Z -> ( F ` y ) = Z ) ) ) )
15 14 com23 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) -> ( y e. dom F -> ( ( G ` y ) = Z -> ( F ` y ) = Z ) ) ) )
16 15 imp31 
 |-  ( ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) /\ y e. dom F ) -> ( ( G ` y ) = Z -> ( F ` y ) = Z ) )
17 16 necon3d 
 |-  ( ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) /\ y e. dom F ) -> ( ( F ` y ) =/= Z -> ( G ` y ) =/= Z ) )
18 17 ex 
 |-  ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) -> ( y e. dom F -> ( ( F ` y ) =/= Z -> ( G ` y ) =/= Z ) ) )
19 18 com23 
 |-  ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) -> ( ( F ` y ) =/= Z -> ( y e. dom F -> ( G ` y ) =/= Z ) ) )
20 19 3imp 
 |-  ( ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) /\ ( F ` y ) =/= Z /\ y e. dom F ) -> ( G ` y ) =/= Z )
21 7 20 rabssrabd 
 |-  ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) -> { y e. dom F | ( F ` y ) =/= Z } C_ { y e. dom G | ( G ` y ) =/= Z } )
22 fnfun 
 |-  ( F Fn A -> Fun F )
23 22 ad2antrr 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> Fun F )
24 simpl 
 |-  ( ( F Fn A /\ G Fn B ) -> F Fn A )
25 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
26 25 3adant3 
 |-  ( ( A C_ B /\ B e. V /\ Z e. W ) -> A e. _V )
27 fnex 
 |-  ( ( F Fn A /\ A e. _V ) -> F e. _V )
28 24 26 27 syl2an 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> F e. _V )
29 simpr3 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> Z e. W )
30 suppval1 
 |-  ( ( Fun F /\ F e. _V /\ Z e. W ) -> ( F supp Z ) = { y e. dom F | ( F ` y ) =/= Z } )
31 23 28 29 30 syl3anc 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( F supp Z ) = { y e. dom F | ( F ` y ) =/= Z } )
32 fnfun 
 |-  ( G Fn B -> Fun G )
33 32 ad2antlr 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> Fun G )
34 simpr 
 |-  ( ( F Fn A /\ G Fn B ) -> G Fn B )
35 simp2 
 |-  ( ( A C_ B /\ B e. V /\ Z e. W ) -> B e. V )
36 fnex 
 |-  ( ( G Fn B /\ B e. V ) -> G e. _V )
37 34 35 36 syl2an 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> G e. _V )
38 suppval1 
 |-  ( ( Fun G /\ G e. _V /\ Z e. W ) -> ( G supp Z ) = { y e. dom G | ( G ` y ) =/= Z } )
39 33 37 29 38 syl3anc 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( G supp Z ) = { y e. dom G | ( G ` y ) =/= Z } )
40 31 39 sseq12d 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( ( F supp Z ) C_ ( G supp Z ) <-> { y e. dom F | ( F ` y ) =/= Z } C_ { y e. dom G | ( G ` y ) =/= Z } ) )
41 40 adantr 
 |-  ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) -> ( ( F supp Z ) C_ ( G supp Z ) <-> { y e. dom F | ( F ` y ) =/= Z } C_ { y e. dom G | ( G ` y ) =/= Z } ) )
42 21 41 mpbird 
 |-  ( ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) /\ A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) ) -> ( F supp Z ) C_ ( G supp Z ) )
43 42 ex 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A C_ B /\ B e. V /\ Z e. W ) ) -> ( A. x e. A ( ( G ` x ) = Z -> ( F ` x ) = Z ) -> ( F supp Z ) C_ ( G supp Z ) ) )