Description: Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elsuppfnd.1 | ⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) | |
elsuppfnd.2 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | ||
elsuppfnd.3 | ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 ) | ||
elsuppfnd.4 | ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 ) | ||
elsuppfnd.5 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) | ||
Assertion | elsuppfnd | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 supp 𝑍 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsuppfnd.1 | ⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) | |
2 | elsuppfnd.2 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
3 | elsuppfnd.3 | ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 ) | |
4 | elsuppfnd.4 | ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 ) | |
5 | elsuppfnd.5 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) | |
6 | elsuppfn | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) ) | |
7 | 6 | biimpar | ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) → 𝑋 ∈ ( 𝐹 supp 𝑍 ) ) |
8 | 1 2 3 4 5 7 | syl32anc | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 supp 𝑍 ) ) |