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

Metamath Proof Explorer

Theorem harsdom

Description: The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harsdom 
|- ( A e. dom card -> A ~< ( har ` A ) )

Proof

Step Hyp Ref Expression
1 harndom 
 |-  -. ( har ` A ) ~<_ A
2 harcl 
 |-  ( har ` A ) e. On
3 onenon 
 |-  ( ( har ` A ) e. On -> ( har ` A ) e. dom card )
4 2 3 ax-mp 
 |-  ( har ` A ) e. dom card
5 domtri2 
 |-  ( ( ( har ` A ) e. dom card /\ A e. dom card ) -> ( ( har ` A ) ~<_ A <-> -. A ~< ( har ` A ) ) )
6 5 con2bid 
 |-  ( ( ( har ` A ) e. dom card /\ A e. dom card ) -> ( A ~< ( har ` A ) <-> -. ( har ` A ) ~<_ A ) )
7 4 6 mpan 
 |-  ( A e. dom card -> ( A ~< ( har ` A ) <-> -. ( har ` A ) ~<_ A ) )
8 1 7 mpbiri 
 |-  ( A e. dom card -> A ~< ( har ` A ) )