Description: A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | f002.1 | |- ( ph -> F : A --> B ) |
|
| Assertion | f002 | |- ( ph -> ( B = (/) -> A = (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f002.1 | |- ( ph -> F : A --> B ) |
|
| 2 | feq3 | |- ( B = (/) -> ( F : A --> B <-> F : A --> (/) ) ) |
|
| 3 | f00 | |- ( F : A --> (/) <-> ( F = (/) /\ A = (/) ) ) |
|
| 4 | 3 | simprbi | |- ( F : A --> (/) -> A = (/) ) |
| 5 | 2 4 | syl6bi | |- ( B = (/) -> ( F : A --> B -> A = (/) ) ) |
| 6 | 1 5 | syl5com | |- ( ph -> ( B = (/) -> A = (/) ) ) |