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 ⊢ V ∈ W ∧ Y ∈ ℕ 0 ∧ V = Y ∧ N ∈ V → Y ∈ ℕ

Proof

Step Hyp Ref Expression
1 ne0i ⊢ N ∈ V → V ≠ ∅
2 hashge1 ⊢ V ∈ W ∧ V ≠ ∅ → 1 ≤ V
3 1 2 sylan2 ⊢ V ∈ W ∧ N ∈ V → 1 ≤ V
4 simpr ⊢ 1 ≤ V ∧ V ∈ ℕ 0 → V ∈ ℕ 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 ⊢ V = 0 → 1 ≤ V ↔ 1 ≤ 0
11 9 10 mtbiri ⊢ V = 0 → ¬ 1 ≤ V
12 11 necon2ai ⊢ 1 ≤ V → V ≠ 0
13 12 adantr ⊢ 1 ≤ V ∧ V ∈ ℕ 0 → V ≠ 0
14 elnnne0 ⊢ V ∈ ℕ ↔ V ∈ ℕ 0 ∧ V ≠ 0
15 4 13 14 sylanbrc ⊢ 1 ≤ V ∧ V ∈ ℕ 0 → V ∈ ℕ
16 15 ex ⊢ 1 ≤ V → V ∈ ℕ 0 → V ∈ ℕ
17 3 16 syl ⊢ V ∈ W ∧ N ∈ V → V ∈ ℕ 0 → V ∈ ℕ
18 17 impancom ⊢ V ∈ W ∧ V ∈ ℕ 0 → N ∈ V → V ∈ ℕ
19 18 com12 ⊢ N ∈ V → V ∈ W ∧ V ∈ ℕ 0 → V ∈ ℕ
20 eleq1 ⊢ V = Y → V ∈ ℕ 0 ↔ Y ∈ ℕ 0
21 20 anbi2d ⊢ V = Y → V ∈ W ∧ V ∈ ℕ 0 ↔ V ∈ W ∧ Y ∈ ℕ 0
22 eleq1 ⊢ V = Y → V ∈ ℕ ↔ Y ∈ ℕ
23 21 22 imbi12d ⊢ V = Y → V ∈ W ∧ V ∈ ℕ 0 → V ∈ ℕ ↔ V ∈ W ∧ Y ∈ ℕ 0 → Y ∈ ℕ
24 19 23 imbitrid ⊢ V = Y → N ∈ V → V ∈ W ∧ Y ∈ ℕ 0 → Y ∈ ℕ
25 24 imp ⊢ V = Y ∧ N ∈ V → V ∈ W ∧ Y ∈ ℕ 0 → Y ∈ ℕ
26 25 impcom ⊢ V ∈ W ∧ Y ∈ ℕ 0 ∧ V = Y ∧ N ∈ V → Y ∈ ℕ