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 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑁 } ) ) = 𝑌 ) )