Metamath Proof Explorer

Theorem suppssr

Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019)

Ref Expression
Hypotheses suppssr.f ⊢ φ → F : A ⟶ B
suppssr.n ⊢ φ → F supp Z ⊆ W
suppssr.a ⊢ φ → A ∈ V
suppssr.z ⊢ φ → Z ∈ U
Assertion suppssr ⊢ φ ∧ X ∈ A ∖ W → F ⁡ X = Z

Proof

Step Hyp Ref Expression
1 suppssr.f ⊢ φ → F : A ⟶ B
2 suppssr.n ⊢ φ → F supp Z ⊆ W
3 suppssr.a ⊢ φ → A ∈ V
4 suppssr.z ⊢ φ → Z ∈ U
5 eldif ⊢ X ∈ A ∖ W ↔ X ∈ A ∧ ¬ X ∈ W
6 fvex ⊢ F ⁡ X ∈ V
7 eldifsn ⊢ F ⁡ X ∈ V ∖ Z ↔ F ⁡ X ∈ V ∧ F ⁡ X ≠ Z
8 6 7 mpbiran ⊢ F ⁡ X ∈ V ∖ Z ↔ F ⁡ X ≠ Z
9 1 ffnd ⊢ φ → F Fn A
10 elsuppfn ⊢ F Fn A ∧ A ∈ V ∧ Z ∈ U → X ∈ supp Z⁡ F ↔ X ∈ A ∧ F ⁡ X ≠ Z
11 9 3 4 10 syl3anc ⊢ φ → X ∈ supp Z⁡ F ↔ X ∈ A ∧ F ⁡ X ≠ Z
12 ibar ⊢ F ⁡ X ∈ V → F ⁡ X ≠ Z ↔ F ⁡ X ∈ V ∧ F ⁡ X ≠ Z
13 6 12 mp1i ⊢ φ ∧ X ∈ A → F ⁡ X ≠ Z ↔ F ⁡ X ∈ V ∧ F ⁡ X ≠ Z
14 13 7 bitr4di ⊢ φ ∧ X ∈ A → F ⁡ X ≠ Z ↔ F ⁡ X ∈ V ∖ Z
15 14 pm5.32da ⊢ φ → X ∈ A ∧ F ⁡ X ≠ Z ↔ X ∈ A ∧ F ⁡ X ∈ V ∖ Z
16 11 15 bitrd ⊢ φ → X ∈ supp Z⁡ F ↔ X ∈ A ∧ F ⁡ X ∈ V ∖ Z
17 2 sseld ⊢ φ → X ∈ supp Z⁡ F → X ∈ W
18 16 17 sylbird ⊢ φ → X ∈ A ∧ F ⁡ X ∈ V ∖ Z → X ∈ W
19 18 expdimp ⊢ φ ∧ X ∈ A → F ⁡ X ∈ V ∖ Z → X ∈ W
20 8 19 syl5bir ⊢ φ ∧ X ∈ A → F ⁡ X ≠ Z → X ∈ W
21 20 necon1bd ⊢ φ ∧ X ∈ A → ¬ X ∈ W → F ⁡ X = Z
22 21 impr ⊢ φ ∧ X ∈ A ∧ ¬ X ∈ W → F ⁡ X = Z
23 5 22 sylan2b ⊢ φ ∧ X ∈ A ∖ W → F ⁡ X = Z