Metamath Proof Explorer

Theorem hashdifsnp1

Description: If the size of a set is a nonnegative integer increased by 1, the size of the set with one of its elements removed is this nonnegative integer. (Contributed by Alexander van der Vekens, 7-Jan-2018)

Ref Expression
Assertion hashdifsnp1 
|- ( ( V e. W /\ N e. V /\ Y e. NN0 ) -> ( ( # ` V ) = ( Y + 1 ) -> ( # ` ( V \ { N } ) ) = Y ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 
 |-  ( Y e. NN0 -> ( Y + 1 ) e. NN0 )
2 eleq1a 
 |-  ( ( Y + 1 ) e. NN0 -> ( ( # ` V ) = ( Y + 1 ) -> ( # ` V ) e. NN0 ) )
3 2 adantr 
 |-  ( ( ( Y + 1 ) e. NN0 /\ V e. W ) -> ( ( # ` V ) = ( Y + 1 ) -> ( # ` V ) e. NN0 ) )
4 3 imp 
 |-  ( ( ( ( Y + 1 ) e. NN0 /\ V e. W ) /\ ( # ` V ) = ( Y + 1 ) ) -> ( # ` V ) e. NN0 )
5 hashclb 
 |-  ( V e. W -> ( V e. Fin <-> ( # ` V ) e. NN0 ) )
6 5 ad2antlr 
 |-  ( ( ( ( Y + 1 ) e. NN0 /\ V e. W ) /\ ( # ` V ) = ( Y + 1 ) ) -> ( V e. Fin <-> ( # ` V ) e. NN0 ) )
7 4 6 mpbird 
 |-  ( ( ( ( Y + 1 ) e. NN0 /\ V e. W ) /\ ( # ` V ) = ( Y + 1 ) ) -> V e. Fin )
8 7 ex 
 |-  ( ( ( Y + 1 ) e. NN0 /\ V e. W ) -> ( ( # ` V ) = ( Y + 1 ) -> V e. Fin ) )
9 8 ex 
 |-  ( ( Y + 1 ) e. NN0 -> ( V e. W -> ( ( # ` V ) = ( Y + 1 ) -> V e. Fin ) ) )
10 1 9 syl 
 |-  ( Y e. NN0 -> ( V e. W -> ( ( # ` V ) = ( Y + 1 ) -> V e. Fin ) ) )
11 10 impcom 
 |-  ( ( V e. W /\ Y e. NN0 ) -> ( ( # ` V ) = ( Y + 1 ) -> V e. Fin ) )
12 11 3adant2 
 |-  ( ( V e. W /\ N e. V /\ Y e. NN0 ) -> ( ( # ` V ) = ( Y + 1 ) -> V e. Fin ) )
13 12 imp 
 |-  ( ( ( V e. W /\ N e. V /\ Y e. NN0 ) /\ ( # ` V ) = ( Y + 1 ) ) -> V e. Fin )
14 snssi 
 |-  ( N e. V -> { N } C_ V )
15 14 3ad2ant2 
 |-  ( ( V e. W /\ N e. V /\ Y e. NN0 ) -> { N } C_ V )
16 15 adantr 
 |-  ( ( ( V e. W /\ N e. V /\ Y e. NN0 ) /\ ( # ` V ) = ( Y + 1 ) ) -> { N } C_ V )
17 hashssdif 
 |-  ( ( V e. Fin /\ { N } C_ V ) -> ( # ` ( V \ { N } ) ) = ( ( # ` V ) - ( # ` { N } ) ) )
18 13 16 17 syl2anc 
 |-  ( ( ( V e. W /\ N e. V /\ Y e. NN0 ) /\ ( # ` V ) = ( Y + 1 ) ) -> ( # ` ( V \ { N } ) ) = ( ( # ` V ) - ( # ` { N } ) ) )
19 oveq1 
 |-  ( ( # ` V ) = ( Y + 1 ) -> ( ( # ` V ) - ( # ` { N } ) ) = ( ( Y + 1 ) - ( # ` { N } ) ) )
20 hashsng 
 |-  ( N e. V -> ( # ` { N } ) = 1 )
21 20 oveq2d 
 |-  ( N e. V -> ( ( Y + 1 ) - ( # ` { N } ) ) = ( ( Y + 1 ) - 1 ) )
22 21 3ad2ant2 
 |-  ( ( V e. W /\ N e. V /\ Y e. NN0 ) -> ( ( Y + 1 ) - ( # ` { N } ) ) = ( ( Y + 1 ) - 1 ) )
23 nn0cn 
 |-  ( Y e. NN0 -> Y e. CC )
24 1cnd 
 |-  ( Y e. NN0 -> 1 e. CC )
25 23 24 pncand 
 |-  ( Y e. NN0 -> ( ( Y + 1 ) - 1 ) = Y )
26 25 3ad2ant3 
 |-  ( ( V e. W /\ N e. V /\ Y e. NN0 ) -> ( ( Y + 1 ) - 1 ) = Y )
27 22 26 eqtrd 
 |-  ( ( V e. W /\ N e. V /\ Y e. NN0 ) -> ( ( Y + 1 ) - ( # ` { N } ) ) = Y )
28 19 27 sylan9eqr 
 |-  ( ( ( V e. W /\ N e. V /\ Y e. NN0 ) /\ ( # ` V ) = ( Y + 1 ) ) -> ( ( # ` V ) - ( # ` { N } ) ) = Y )
29 18 28 eqtrd 
 |-  ( ( ( V e. W /\ N e. V /\ Y e. NN0 ) /\ ( # ` V ) = ( Y + 1 ) ) -> ( # ` ( V \ { N } ) ) = Y )
30 29 ex 
 |-  ( ( V e. W /\ N e. V /\ Y e. NN0 ) -> ( ( # ` V ) = ( Y + 1 ) -> ( # ` ( V \ { N } ) ) = Y ) )