Theorem hashnn0n0nn

Description: If a nonnegative integer is the size of a set which contains at least one element, this integer is a positive integer. (Contributed by Alexander van der Vekens, 9-Jan-2018)

	Ref	Expression
Assertion	hashnn0n0nn	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) ) → 𝑌 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 𝑁 ∈ 𝑉 → 𝑉 ≠ ∅ )
2		hashge1	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝑉 ) )
3	1 2	sylan2	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ) → 1 ≤ ( ♯ ‘ 𝑉 ) )
4		simpr	⊢ ( ( 1 ≤ ( ♯ ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
5		0lt1	⊢ 0 < 1
6		0re	⊢ 0 ∈ ℝ
7		1re	⊢ 1 ∈ ℝ
8	6 7	ltnlei	⊢ ( 0 < 1 ↔ ¬ 1 ≤ 0 )
9	5 8	mpbi	⊢ ¬ 1 ≤ 0
10		breq2	⊢ ( ( ♯ ‘ 𝑉 ) = 0 → ( 1 ≤ ( ♯ ‘ 𝑉 ) ↔ 1 ≤ 0 ) )
11	9 10	mtbiri	⊢ ( ( ♯ ‘ 𝑉 ) = 0 → ¬ 1 ≤ ( ♯ ‘ 𝑉 ) )
12	11	necon2ai	⊢ ( 1 ≤ ( ♯ ‘ 𝑉 ) → ( ♯ ‘ 𝑉 ) ≠ 0 )
13	12	adantr	⊢ ( ( 1 ≤ ( ♯ ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) → ( ♯ ‘ 𝑉 ) ≠ 0 )
14		elnnne0	⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) )
15	4 13 14	sylanbrc	⊢ ( ( 1 ≤ ( ♯ ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) → ( ♯ ‘ 𝑉 ) ∈ ℕ )
16	15	ex	⊢ ( 1 ≤ ( ♯ ‘ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ♯ ‘ 𝑉 ) ∈ ℕ ) )
17	3 16	syl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ♯ ‘ 𝑉 ) ∈ ℕ ) )
18	17	impancom	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) → ( 𝑁 ∈ 𝑉 → ( ♯ ‘ 𝑉 ) ∈ ℕ ) )
19	18	com12	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) → ( ♯ ‘ 𝑉 ) ∈ ℕ ) )
20		eleq1	⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ↔ 𝑌 ∈ ℕ0 ) )
21	20	anbi2d	⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) ↔ ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) ) )
22		eleq1	⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( ( ♯ ‘ 𝑉 ) ∈ ℕ ↔ 𝑌 ∈ ℕ ) )
23	21 22	imbi12d	⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) → ( ♯ ‘ 𝑉 ) ∈ ℕ ) ↔ ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) → 𝑌 ∈ ℕ ) ) )
24	19 23	syl5ib	⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) → 𝑌 ∈ ℕ ) ) )
25	24	imp	⊢ ( ( ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) → 𝑌 ∈ ℕ ) )
26	25	impcom	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) ) → 𝑌 ∈ ℕ )