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 𝑍 ) ) |