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 ‘ 𝐴 ) ) |
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 ‘ 𝐴 ) ) |