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

Metamath Proof Explorer

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 imbitrid ⊢ ( ( ♯ ‘ 𝑉 ) = 𝑌 → ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) → 𝑌 ∈ ℕ ) ) )
25 24 imp ⊢ ( ( ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) → 𝑌 ∈ ℕ ) )
26 25 impcom ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝑉 ) = 𝑌 ∧ 𝑁 ∈ 𝑉 ) ) → 𝑌 ∈ ℕ )