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 ∧ 𝑌 ≼ 𝑋 ) )