Metamath Proof Explorer


Theorem suppcoss

Description: The support of the composition of two functions is a subset of the support of the inner function if the outer function preserves zero. Compare suppssfv , which has a sethood condition on A instead of B . (Contributed by SN, 25-May-2024)

Ref Expression
Hypotheses suppcoss.f φ F Fn A
suppcoss.g φ G : B A
suppcoss.b φ B W
suppcoss.y φ Y V
suppcoss.1 φ F Y = Z
Assertion suppcoss φ F G supp Z G supp Y

Proof

Step Hyp Ref Expression
1 suppcoss.f φ F Fn A
2 suppcoss.g φ G : B A
3 suppcoss.b φ B W
4 suppcoss.y φ Y V
5 suppcoss.1 φ F Y = Z
6 dffn3 F Fn A F : A ran F
7 1 6 sylib φ F : A ran F
8 7 2 fcod φ F G : B ran F
9 eldif k B supp Y G k B ¬ k supp Y G
10 2 ffnd φ G Fn B
11 elsuppfn G Fn B B W Y V k supp Y G k B G k Y
12 10 3 4 11 syl3anc φ k supp Y G k B G k Y
13 12 notbid φ ¬ k supp Y G ¬ k B G k Y
14 13 anbi2d φ k B ¬ k supp Y G k B ¬ k B G k Y
15 annotanannot k B ¬ k B G k Y k B ¬ G k Y
16 14 15 bitrdi φ k B ¬ k supp Y G k B ¬ G k Y
17 9 16 syl5bb φ k B supp Y G k B ¬ G k Y
18 nne ¬ G k Y G k = Y
19 18 anbi2i k B ¬ G k Y k B G k = Y
20 2 adantr φ k B G k = Y G : B A
21 simprl φ k B G k = Y k B
22 20 21 fvco3d φ k B G k = Y F G k = F G k
23 simprr φ k B G k = Y G k = Y
24 23 fveq2d φ k B G k = Y F G k = F Y
25 5 adantr φ k B G k = Y F Y = Z
26 22 24 25 3eqtrd φ k B G k = Y F G k = Z
27 26 ex φ k B G k = Y F G k = Z
28 19 27 syl5bi φ k B ¬ G k Y F G k = Z
29 17 28 sylbid φ k B supp Y G F G k = Z
30 29 imp φ k B supp Y G F G k = Z
31 8 30 suppss φ F G supp Z G supp Y