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 \in har (X) \leftrightarrow (Y \in On \land Y ≼ X)$

Proof

Step	Hyp	Ref	Expression
1		elfvex	$⊢ Y \in har (X) \to X \in V$
2		reldom	$⊢ Rel ≼$
3	2	brrelex2i	$⊢ Y ≼ X \to X \in V$
4	3	adantl	$⊢ (Y \in On \land Y ≼ X) \to X \in V$
5		harval	$⊢ X \in V \to har (X) = \{y \in On \| y ≼ X\}$
6	5	eleq2d	$⊢ X \in V \to (Y \in har (X) \leftrightarrow Y \in \{y \in On \| y ≼ X\})$
7		breq1	$⊢ y = Y \to (y ≼ X \leftrightarrow Y ≼ X)$
8	7	elrab	$⊢ Y \in \{y \in On \| y ≼ X\} \leftrightarrow (Y \in On \land Y ≼ X)$
9	6 8	bitrdi	$⊢ X \in V \to (Y \in har (X) \leftrightarrow (Y \in On \land Y ≼ X))$
10	1 4 9	pm5.21nii	$⊢ Y \in har (X) \leftrightarrow (Y \in On \land Y ≼ X)$

Metamath Proof Explorer

Theorem elharval

Proof