This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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