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

Metamath Proof Explorer

Theorem hashsdom

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

Ref Expression
Assertion hashsdom ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≺ 𝐵 ) )

Proof

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