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	syl5bb	⊢ ( ( 𝐴 ∈ 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 ) → ( ( ♯ ‘ 𝐴 ) < ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≺ 𝐵 ) )