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

Metamath Proof Explorer

Theorem harsdom

Description: The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harsdom ⊢ A ∈ dom ⁡ card → A ≺ har ⁡ A

Proof

Step Hyp Ref Expression
1 harndom ⊢ ¬ har ⁡ A ≼ A
2 harcl ⊢ har ⁡ A ∈ On
3 onenon ⊢ har ⁡ A ∈ On → har ⁡ A ∈ dom ⁡ card
4 2 3 ax-mp ⊢ har ⁡ A ∈ dom ⁡ card
5 domtri2 ⊢ har ⁡ A ∈ dom ⁡ card ∧ A ∈ dom ⁡ card → har ⁡ A ≼ A ↔ ¬ A ≺ har ⁡ A
6 5 con2bid ⊢ har ⁡ A ∈ dom ⁡ card ∧ A ∈ dom ⁡ card → A ≺ har ⁡ A ↔ ¬ har ⁡ A ≼ A
7 4 6 mpan ⊢ A ∈ dom ⁡ card → A ≺ har ⁡ A ↔ ¬ har ⁡ A ≼ A
8 1 7 mpbiri ⊢ A ∈ dom ⁡ card → A ≺ har ⁡ A