Theorem onsdom

Description: Any well-orderable set is strictly dominated by an ordinal number. (Contributed by Jeff Hankins, 22-Oct-2009) (Proof shortened by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	onsdom	⊢ ( 𝐴 ∈ dom card → ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		harcl	⊢ ( har ‘ 𝐴 ) ∈ On
2		harsdom	⊢ ( 𝐴 ∈ dom card → 𝐴 ≺ ( har ‘ 𝐴 ) )
3		breq2	⊢ ( 𝑥 = ( har ‘ 𝐴 ) → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ ( har ‘ 𝐴 ) ) )
4	3	rspcev	⊢ ( ( ( har ‘ 𝐴 ) ∈ On ∧ 𝐴 ≺ ( har ‘ 𝐴 ) ) → ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 )
5	1 2 4	sylancr	⊢ ( 𝐴 ∈ dom card → ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 )