# 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 ${⊢}\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\to \left(\left|{V}\right|={Y}+1\to \left|{V}\setminus \left\{{N}\right\}\right|={Y}\right)$

### Proof

Step Hyp Ref Expression
1 peano2nn0 ${⊢}{Y}\in {ℕ}_{0}\to {Y}+1\in {ℕ}_{0}$
2 eleq1a ${⊢}{Y}+1\in {ℕ}_{0}\to \left(\left|{V}\right|={Y}+1\to \left|{V}\right|\in {ℕ}_{0}\right)$
3 2 adantr ${⊢}\left({Y}+1\in {ℕ}_{0}\wedge {V}\in {W}\right)\to \left(\left|{V}\right|={Y}+1\to \left|{V}\right|\in {ℕ}_{0}\right)$
4 3 imp ${⊢}\left(\left({Y}+1\in {ℕ}_{0}\wedge {V}\in {W}\right)\wedge \left|{V}\right|={Y}+1\right)\to \left|{V}\right|\in {ℕ}_{0}$
5 hashclb ${⊢}{V}\in {W}\to \left({V}\in \mathrm{Fin}↔\left|{V}\right|\in {ℕ}_{0}\right)$
6 5 ad2antlr ${⊢}\left(\left({Y}+1\in {ℕ}_{0}\wedge {V}\in {W}\right)\wedge \left|{V}\right|={Y}+1\right)\to \left({V}\in \mathrm{Fin}↔\left|{V}\right|\in {ℕ}_{0}\right)$
7 4 6 mpbird ${⊢}\left(\left({Y}+1\in {ℕ}_{0}\wedge {V}\in {W}\right)\wedge \left|{V}\right|={Y}+1\right)\to {V}\in \mathrm{Fin}$
8 7 ex ${⊢}\left({Y}+1\in {ℕ}_{0}\wedge {V}\in {W}\right)\to \left(\left|{V}\right|={Y}+1\to {V}\in \mathrm{Fin}\right)$
9 8 ex ${⊢}{Y}+1\in {ℕ}_{0}\to \left({V}\in {W}\to \left(\left|{V}\right|={Y}+1\to {V}\in \mathrm{Fin}\right)\right)$
10 1 9 syl ${⊢}{Y}\in {ℕ}_{0}\to \left({V}\in {W}\to \left(\left|{V}\right|={Y}+1\to {V}\in \mathrm{Fin}\right)\right)$
11 10 impcom ${⊢}\left({V}\in {W}\wedge {Y}\in {ℕ}_{0}\right)\to \left(\left|{V}\right|={Y}+1\to {V}\in \mathrm{Fin}\right)$
12 11 3adant2 ${⊢}\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\to \left(\left|{V}\right|={Y}+1\to {V}\in \mathrm{Fin}\right)$
13 12 imp ${⊢}\left(\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\wedge \left|{V}\right|={Y}+1\right)\to {V}\in \mathrm{Fin}$
14 snssi ${⊢}{N}\in {V}\to \left\{{N}\right\}\subseteq {V}$
15 14 3ad2ant2 ${⊢}\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\to \left\{{N}\right\}\subseteq {V}$
16 15 adantr ${⊢}\left(\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\wedge \left|{V}\right|={Y}+1\right)\to \left\{{N}\right\}\subseteq {V}$
17 hashssdif ${⊢}\left({V}\in \mathrm{Fin}\wedge \left\{{N}\right\}\subseteq {V}\right)\to \left|{V}\setminus \left\{{N}\right\}\right|=\left|{V}\right|-\left|\left\{{N}\right\}\right|$
18 13 16 17 syl2anc ${⊢}\left(\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\wedge \left|{V}\right|={Y}+1\right)\to \left|{V}\setminus \left\{{N}\right\}\right|=\left|{V}\right|-\left|\left\{{N}\right\}\right|$
19 oveq1 ${⊢}\left|{V}\right|={Y}+1\to \left|{V}\right|-\left|\left\{{N}\right\}\right|={Y}+1-\left|\left\{{N}\right\}\right|$
20 hashsng ${⊢}{N}\in {V}\to \left|\left\{{N}\right\}\right|=1$
21 20 oveq2d ${⊢}{N}\in {V}\to {Y}+1-\left|\left\{{N}\right\}\right|={Y}+1-1$
22 21 3ad2ant2 ${⊢}\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\to {Y}+1-\left|\left\{{N}\right\}\right|={Y}+1-1$
23 nn0cn ${⊢}{Y}\in {ℕ}_{0}\to {Y}\in ℂ$
24 1cnd ${⊢}{Y}\in {ℕ}_{0}\to 1\in ℂ$
25 23 24 pncand ${⊢}{Y}\in {ℕ}_{0}\to {Y}+1-1={Y}$
26 25 3ad2ant3 ${⊢}\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\to {Y}+1-1={Y}$
27 22 26 eqtrd ${⊢}\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\to {Y}+1-\left|\left\{{N}\right\}\right|={Y}$
28 19 27 sylan9eqr ${⊢}\left(\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\wedge \left|{V}\right|={Y}+1\right)\to \left|{V}\right|-\left|\left\{{N}\right\}\right|={Y}$
29 18 28 eqtrd ${⊢}\left(\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\wedge \left|{V}\right|={Y}+1\right)\to \left|{V}\setminus \left\{{N}\right\}\right|={Y}$
30 29 ex ${⊢}\left({V}\in {W}\wedge {N}\in {V}\wedge {Y}\in {ℕ}_{0}\right)\to \left(\left|{V}\right|={Y}+1\to \left|{V}\setminus \left\{{N}\right\}\right|={Y}\right)$