# 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 ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = 𝑌 ) )

### Proof

Step Hyp Ref Expression
1 peano2nn0 ( 𝑌 ∈ ℕ0 → ( 𝑌 + 1 ) ∈ ℕ0 )
2 eleq1a ( ( 𝑌 + 1 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) )
3 2 adantr ( ( ( 𝑌 + 1 ) ∈ ℕ0𝑉𝑊 ) → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) )
4 3 imp ( ( ( ( 𝑌 + 1 ) ∈ ℕ0𝑉𝑊 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
5 hashclb ( 𝑉𝑊 → ( 𝑉 ∈ Fin ↔ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) )
6 5 ad2antlr ( ( ( ( 𝑌 + 1 ) ∈ ℕ0𝑉𝑊 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → ( 𝑉 ∈ Fin ↔ ( ♯ ‘ 𝑉 ) ∈ ℕ0 ) )
7 4 6 mpbird ( ( ( ( 𝑌 + 1 ) ∈ ℕ0𝑉𝑊 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → 𝑉 ∈ Fin )
8 7 ex ( ( ( 𝑌 + 1 ) ∈ ℕ0𝑉𝑊 ) → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → 𝑉 ∈ Fin ) )
9 8 ex ( ( 𝑌 + 1 ) ∈ ℕ0 → ( 𝑉𝑊 → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → 𝑉 ∈ Fin ) ) )
10 1 9 syl ( 𝑌 ∈ ℕ0 → ( 𝑉𝑊 → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → 𝑉 ∈ Fin ) ) )
11 10 impcom ( ( 𝑉𝑊𝑌 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → 𝑉 ∈ Fin ) )
12 11 3adant2 ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → 𝑉 ∈ Fin ) )
13 12 imp ( ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → 𝑉 ∈ Fin )
14 snssi ( 𝑁𝑉 → { 𝑁 } ⊆ 𝑉 )
15 14 3ad2ant2 ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) → { 𝑁 } ⊆ 𝑉 )
16 15 adantr ( ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → { 𝑁 } ⊆ 𝑉 )
17 hashssdif ( ( 𝑉 ∈ Fin ∧ { 𝑁 } ⊆ 𝑉 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − ( ♯ ‘ { 𝑁 } ) ) )
18 13 16 17 syl2anc ( ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = ( ( ♯ ‘ 𝑉 ) − ( ♯ ‘ { 𝑁 } ) ) )
19 oveq1 ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → ( ( ♯ ‘ 𝑉 ) − ( ♯ ‘ { 𝑁 } ) ) = ( ( 𝑌 + 1 ) − ( ♯ ‘ { 𝑁 } ) ) )
20 hashsng ( 𝑁𝑉 → ( ♯ ‘ { 𝑁 } ) = 1 )
21 20 oveq2d ( 𝑁𝑉 → ( ( 𝑌 + 1 ) − ( ♯ ‘ { 𝑁 } ) ) = ( ( 𝑌 + 1 ) − 1 ) )
22 21 3ad2ant2 ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) → ( ( 𝑌 + 1 ) − ( ♯ ‘ { 𝑁 } ) ) = ( ( 𝑌 + 1 ) − 1 ) )
23 nn0cn ( 𝑌 ∈ ℕ0𝑌 ∈ ℂ )
24 1cnd ( 𝑌 ∈ ℕ0 → 1 ∈ ℂ )
25 23 24 pncand ( 𝑌 ∈ ℕ0 → ( ( 𝑌 + 1 ) − 1 ) = 𝑌 )
26 25 3ad2ant3 ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) → ( ( 𝑌 + 1 ) − 1 ) = 𝑌 )
27 22 26 eqtrd ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) → ( ( 𝑌 + 1 ) − ( ♯ ‘ { 𝑁 } ) ) = 𝑌 )
28 19 27 sylan9eqr ( ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → ( ( ♯ ‘ 𝑉 ) − ( ♯ ‘ { 𝑁 } ) ) = 𝑌 )
29 18 28 eqtrd ( ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = 𝑌 )
30 29 ex ( ( 𝑉𝑊𝑁𝑉𝑌 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) = ( 𝑌 + 1 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = 𝑌 ) )