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 syl5ib ⊢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∈ℕ