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 bitrid ⊢ φ → 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 biimtrid ⊢ φ → 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