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