This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ∈ dom ⁡ card → ∃ x ∈ On A ≺ x

Proof

Step Hyp Ref Expression
1 harcl ⊢ har ⁡ A ∈ On
2 harsdom ⊢ A ∈ dom ⁡ card → A ≺ har ⁡ A
3 breq2 ⊢ x = har ⁡ A → A ≺ x ↔ A ≺ har ⁡ A
4 3 rspcev ⊢ har ⁡ A ∈ On ∧ A ≺ har ⁡ A → ∃ x ∈ On A ≺ x
5 1 2 4 sylancr ⊢ A ∈ dom ⁡ card → ∃ x ∈ On A ≺ x