This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem harndom

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

Proof

Step Hyp Ref Expression
1 harcl ⊢ har ⁡ X ∈ On
2 1 onirri ⊢ ¬ har ⁡ X ∈ har ⁡ X
3 elharval ⊢ har ⁡ X ∈ har ⁡ X ↔ har ⁡ X ∈ On ∧ har ⁡ X ≼ X
4 1 3 mpbiran ⊢ har ⁡ X ∈ har ⁡ X ↔ har ⁡ X ≼ X
5 2 4 mtbi ⊢ ¬ har ⁡ X ≼ X