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 ∈ W ∧ N ∈ V ∧ Y ∈ ℕ 0 → V = Y + 1 → V ∖ N = Y

Proof

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