Description: When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of Mendelson p. 255. (Contributed by NM, 8-Dec-2003)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mapprc | |- ( -. A e. _V -> { f | f : A --> B } = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abn0 | |- ( { f | f : A --> B } =/= (/) <-> E. f f : A --> B ) |
|
| 2 | fdm | |- ( f : A --> B -> dom f = A ) |
|
| 3 | vex | |- f e. _V |
|
| 4 | 3 | dmex | |- dom f e. _V |
| 5 | 2 4 | eqeltrrdi | |- ( f : A --> B -> A e. _V ) |
| 6 | 5 | exlimiv | |- ( E. f f : A --> B -> A e. _V ) |
| 7 | 1 6 | sylbi | |- ( { f | f : A --> B } =/= (/) -> A e. _V ) |
| 8 | 7 | necon1bi | |- ( -. A e. _V -> { f | f : A --> B } = (/) ) |