Theorem hashne0

Description: Deduce that the size of a set is not zero. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	hashne0.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	hashne0.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	hashne0	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		hashne0.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		hashne0.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		hashxnn0	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0* )
4	1 3	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0* )
5		hasheq0	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
6	5	necon3bid	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ ∅ ) )
7	6	biimpar	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ≠ 0 )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ≠ 0 )
9		xnn0gt0	⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0* ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) → 0 < ( ♯ ‘ 𝐴 ) )
10	4 8 9	syl2anc	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐴 ) )