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 ) )