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 ( 𝐴 ∈ dom card → 𝐴 ≺ ( har ‘ 𝐴 ) )

Proof

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