Description: Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | elsuppfnd.1 | |- ( ph -> F Fn A ) |
|
| elsuppfnd.2 | |- ( ph -> A e. V ) |
||
| elsuppfnd.3 | |- ( ph -> Z e. W ) |
||
| elsuppfnd.4 | |- ( ph -> X e. A ) |
||
| elsuppfnd.5 | |- ( ph -> ( F ` X ) =/= Z ) |
||
| Assertion | elsuppfnd | |- ( ph -> X e. ( F supp Z ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elsuppfnd.1 | |- ( ph -> F Fn A ) |
|
| 2 | elsuppfnd.2 | |- ( ph -> A e. V ) |
|
| 3 | elsuppfnd.3 | |- ( ph -> Z e. W ) |
|
| 4 | elsuppfnd.4 | |- ( ph -> X e. A ) |
|
| 5 | elsuppfnd.5 | |- ( ph -> ( F ` X ) =/= Z ) |
|
| 6 | elsuppfn | |- ( ( F Fn A /\ A e. V /\ Z e. W ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) ) |
|
| 7 | 6 | biimpar | |- ( ( ( F Fn A /\ A e. V /\ Z e. W ) /\ ( X e. A /\ ( F ` X ) =/= Z ) ) -> X e. ( F supp Z ) ) |
| 8 | 1 2 3 4 5 7 | syl32anc | |- ( ph -> X e. ( F supp Z ) ) |