Metamath Proof Explorer

Theorem hashnnltb

Description: The # function on _om preserves the ordering. (Contributed by Eric Schmidt, 7-Jul-2026)

Ref Expression
Assertion hashnnltb ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B ↔ A < B

Proof

Step Hyp Ref Expression
1 hashnnlt ⊢ B ∈ ω ∧ A ∈ B → A < B
2 1 ex ⊢ B ∈ ω → A ∈ B → A < B
3 2 adantl ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B → A < B
4 hashss ⊢ A ∈ ω ∧ B ⊆ A → B ≤ A
5 4 ex ⊢ A ∈ ω → B ⊆ A → B ≤ A
6 5 adantr ⊢ A ∈ ω ∧ B ∈ ω → B ⊆ A → B ≤ A
7 nnon ⊢ B ∈ ω → B ∈ On
8 nnon ⊢ A ∈ ω → A ∈ On
9 ontri1 ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ ¬ A ∈ B
10 7 8 9 syl2anr ⊢ A ∈ ω ∧ B ∈ ω → B ⊆ A ↔ ¬ A ∈ B
11 hashxrcl ⊢ B ∈ ω → B ∈ ℝ *
12 hashxrcl ⊢ A ∈ ω → A ∈ ℝ *
13 xrlenlt ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B ≤ A ↔ ¬ A < B
14 11 12 13 syl2anr ⊢ A ∈ ω ∧ B ∈ ω → B ≤ A ↔ ¬ A < B
15 6 10 14 3imtr3d ⊢ A ∈ ω ∧ B ∈ ω → ¬ A ∈ B → ¬ A < B
16 3 15 impcon4bid ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B ↔ A < B