Description: The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 15-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | harndom | |- -. ( har ` X ) ~<_ X |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | harcl | |- ( har ` X ) e. On |
|
| 2 | 1 | onirri | |- -. ( har ` X ) e. ( har ` X ) |
| 3 | elharval | |- ( ( har ` X ) e. ( har ` X ) <-> ( ( har ` X ) e. On /\ ( har ` X ) ~<_ X ) ) |
|
| 4 | 1 3 | mpbiran | |- ( ( har ` X ) e. ( har ` X ) <-> ( har ` X ) ~<_ X ) |
| 5 | 2 4 | mtbi | |- -. ( har ` X ) ~<_ X |