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 ( 𝑌 ∈ ( har ‘ 𝑋 ) ↔ ( 𝑌 ∈ On ∧ 𝑌𝑋 ) )

Proof

Step Hyp Ref Expression
1 elfvex ( 𝑌 ∈ ( har ‘ 𝑋 ) → 𝑋 ∈ V )
2 reldom Rel ≼
3 2 brrelex2i ( 𝑌𝑋𝑋 ∈ V )
4 3 adantl ( ( 𝑌 ∈ On ∧ 𝑌𝑋 ) → 𝑋 ∈ V )
5 harval ( 𝑋 ∈ V → ( har ‘ 𝑋 ) = { 𝑦 ∈ On ∣ 𝑦𝑋 } )
6 5 eleq2d ( 𝑋 ∈ V → ( 𝑌 ∈ ( har ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑦 ∈ On ∣ 𝑦𝑋 } ) )
7 breq1 ( 𝑦 = 𝑌 → ( 𝑦𝑋𝑌𝑋 ) )
8 7 elrab ( 𝑌 ∈ { 𝑦 ∈ On ∣ 𝑦𝑋 } ↔ ( 𝑌 ∈ On ∧ 𝑌𝑋 ) )
9 6 8 bitrdi ( 𝑋 ∈ V → ( 𝑌 ∈ ( har ‘ 𝑋 ) ↔ ( 𝑌 ∈ On ∧ 𝑌𝑋 ) ) )
10 1 4 9 pm5.21nii ( 𝑌 ∈ ( har ‘ 𝑋 ) ↔ ( 𝑌 ∈ On ∧ 𝑌𝑋 ) )