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

Metamath Proof Explorer

Theorem elharval

Description: The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl , this implies that the Hartogs number of a set is greater than all ordinals that set dominates. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion elharval 
|- ( Y e. ( har ` X ) <-> ( Y e. On /\ Y ~<_ X ) )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( Y e. ( har ` X ) -> X e. _V )
2 reldom 
 |-  Rel ~<_
3 2 brrelex2i 
 |-  ( Y ~<_ X -> X e. _V )
4 3 adantl 
 |-  ( ( Y e. On /\ Y ~<_ X ) -> X e. _V )
5 harval 
 |-  ( X e. _V -> ( har ` X ) = { y e. On | y ~<_ X } )
6 5 eleq2d 
 |-  ( X e. _V -> ( Y e. ( har ` X ) <-> Y e. { y e. On | y ~<_ X } ) )
7 breq1 
 |-  ( y = Y -> ( y ~<_ X <-> Y ~<_ X ) )
8 7 elrab 
 |-  ( Y e. { y e. On | y ~<_ X } <-> ( Y e. On /\ Y ~<_ X ) )
9 6 8 bitrdi 
 |-  ( X e. _V -> ( Y e. ( har ` X ) <-> ( Y e. On /\ Y ~<_ X ) ) )
10 1 4 9 pm5.21nii 
 |-  ( Y e. ( har ` X ) <-> ( Y e. On /\ Y ~<_ X ) )