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 
|- ( ( ( V e. W /\ Y e. NN0 ) /\ ( ( # ` V ) = Y /\ N e. V ) ) -> Y e. NN )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( N e. V -> V =/= (/) )
2 hashge1 
 |-  ( ( V e. W /\ V =/= (/) ) -> 1 <_ ( # ` V ) )
3 1 2 sylan2 
 |-  ( ( V e. W /\ N e. V ) -> 1 <_ ( # ` V ) )
4 simpr 
 |-  ( ( 1 <_ ( # ` V ) /\ ( # ` V ) e. NN0 ) -> ( # ` V ) e. NN0 )
5 0lt1 
 |-  0 < 1
6 0re 
 |-  0 e. RR
7 1re 
 |-  1 e. RR
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 ) e. NN0 ) -> ( # ` V ) =/= 0 )
14 elnnne0 
 |-  ( ( # ` V ) e. NN <-> ( ( # ` V ) e. NN0 /\ ( # ` V ) =/= 0 ) )
15 4 13 14 sylanbrc 
 |-  ( ( 1 <_ ( # ` V ) /\ ( # ` V ) e. NN0 ) -> ( # ` V ) e. NN )
16 15 ex 
 |-  ( 1 <_ ( # ` V ) -> ( ( # ` V ) e. NN0 -> ( # ` V ) e. NN ) )
17 3 16 syl 
 |-  ( ( V e. W /\ N e. V ) -> ( ( # ` V ) e. NN0 -> ( # ` V ) e. NN ) )
18 17 impancom 
 |-  ( ( V e. W /\ ( # ` V ) e. NN0 ) -> ( N e. V -> ( # ` V ) e. NN ) )
19 18 com12 
 |-  ( N e. V -> ( ( V e. W /\ ( # ` V ) e. NN0 ) -> ( # ` V ) e. NN ) )
20 eleq1 
 |-  ( ( # ` V ) = Y -> ( ( # ` V ) e. NN0 <-> Y e. NN0 ) )
21 20 anbi2d 
 |-  ( ( # ` V ) = Y -> ( ( V e. W /\ ( # ` V ) e. NN0 ) <-> ( V e. W /\ Y e. NN0 ) ) )
22 eleq1 
 |-  ( ( # ` V ) = Y -> ( ( # ` V ) e. NN <-> Y e. NN ) )
23 21 22 imbi12d 
 |-  ( ( # ` V ) = Y -> ( ( ( V e. W /\ ( # ` V ) e. NN0 ) -> ( # ` V ) e. NN ) <-> ( ( V e. W /\ Y e. NN0 ) -> Y e. NN ) ) )
24 19 23 imbitrid 
 |-  ( ( # ` V ) = Y -> ( N e. V -> ( ( V e. W /\ Y e. NN0 ) -> Y e. NN ) ) )
25 24 imp 
 |-  ( ( ( # ` V ) = Y /\ N e. V ) -> ( ( V e. W /\ Y e. NN0 ) -> Y e. NN ) )
26 25 impcom 
 |-  ( ( ( V e. W /\ Y e. NN0 ) /\ ( ( # ` V ) = Y /\ N e. V ) ) -> Y e. NN )