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 ∈ har ⁡ X ↔ Y ∈ On ∧ Y ≼ X

Proof

Step Hyp Ref Expression
1 elfvex ⊢ Y ∈ har ⁡ X → X ∈ V
2 reldom ⊢ Rel ⁡ ≼
3 2 brrelex2i ⊢ Y ≼ X → X ∈ V
4 3 adantl ⊢ Y ∈ On ∧ Y ≼ X → X ∈ V
5 harval ⊢ X ∈ V → har ⁡ X = y ∈ On | y ≼ X
6 5 eleq2d ⊢ X ∈ V → Y ∈ har ⁡ X ↔ Y ∈ y ∈ On | y ≼ X
7 breq1 ⊢ y = Y → y ≼ X ↔ Y ≼ X
8 7 elrab ⊢ Y ∈ y ∈ On | y ≼ X ↔ Y ∈ On ∧ Y ≼ X
9 6 8 bitrdi ⊢ X ∈ V → Y ∈ har ⁡ X ↔ Y ∈ On ∧ Y ≼ X
10 1 4 9 pm5.21nii ⊢ Y ∈ har ⁡ X ↔ Y ∈ On ∧ Y ≼ X