Metamath Proof Explorer

Theorem hashsdom

Description: Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion hashsdom ⊢ A ∈ Fin ∧ B ∈ Fin → A < B ↔ A ≺ B

Proof

Step Hyp Ref Expression
1 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
2 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
3 nn0re ⊢ A ∈ ℕ 0 → A ∈ ℝ
4 nn0re ⊢ B ∈ ℕ 0 → B ∈ ℝ
5 ltlen ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A ≤ B ∧ B ≠ A
6 3 4 5 syl2an ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → A < B ↔ A ≤ B ∧ B ≠ A
7 1 2 6 syl2an ⊢ A ∈ Fin ∧ B ∈ Fin → A < B ↔ A ≤ B ∧ B ≠ A
8 hashdom ⊢ A ∈ Fin ∧ B ∈ Fin → A ≤ B ↔ A ≼ B
9 eqcom ⊢ B = A ↔ A = B
10 hashen ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ A ≈ B
11 9 10 syl5bb ⊢ A ∈ Fin ∧ B ∈ Fin → B = A ↔ A ≈ B
12 11 necon3abid ⊢ A ∈ Fin ∧ B ∈ Fin → B ≠ A ↔ ¬ A ≈ B
13 8 12 anbi12d ⊢ A ∈ Fin ∧ B ∈ Fin → A ≤ B ∧ B ≠ A ↔ A ≼ B ∧ ¬ A ≈ B
14 7 13 bitrd ⊢ A ∈ Fin ∧ B ∈ Fin → A < B ↔ A ≼ B ∧ ¬ A ≈ B
15 brsdom ⊢ A ≺ B ↔ A ≼ B ∧ ¬ A ≈ B
16 14 15 bitr4di ⊢ A ∈ Fin ∧ B ∈ Fin → A < B ↔ A ≺ B