Description: Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ffs2.1 | ⊢ 𝐶 = ( 𝐵 ∖ { 𝑍 } ) | |
| Assertion | ffs2 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ 𝐶 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ffs2.1 | ⊢ 𝐶 = ( 𝐵 ∖ { 𝑍 } ) | |
| 2 | fsuppeq | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) ) ) | |
| 3 | 2 | 3impia | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) ) |
| 4 | 1 | imaeq2i | ⊢ ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ ( 𝐵 ∖ { 𝑍 } ) ) |
| 5 | 3 4 | eqtr4di | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ 𝐶 ) ) |