# Metamath Proof Explorer

## Theorem hashdifpr

Description: The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020)

Ref Expression
Assertion hashdifpr ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|{A}\setminus \left\{{B},{C}\right\}\right|=\left|{A}\right|-2$

### Proof

Step Hyp Ref Expression
1 difpr ${⊢}{A}\setminus \left\{{B},{C}\right\}=\left({A}\setminus \left\{{B}\right\}\right)\setminus \left\{{C}\right\}$
2 1 a1i ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to {A}\setminus \left\{{B},{C}\right\}=\left({A}\setminus \left\{{B}\right\}\right)\setminus \left\{{C}\right\}$
3 2 fveq2d ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|{A}\setminus \left\{{B},{C}\right\}\right|=\left|\left({A}\setminus \left\{{B}\right\}\right)\setminus \left\{{C}\right\}\right|$
4 diffi ${⊢}{A}\in \mathrm{Fin}\to {A}\setminus \left\{{B}\right\}\in \mathrm{Fin}$
5 necom ${⊢}{B}\ne {C}↔{C}\ne {B}$
6 5 biimpi ${⊢}{B}\ne {C}\to {C}\ne {B}$
7 6 anim2i ${⊢}\left({C}\in {A}\wedge {B}\ne {C}\right)\to \left({C}\in {A}\wedge {C}\ne {B}\right)$
8 7 3adant1 ${⊢}\left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\to \left({C}\in {A}\wedge {C}\ne {B}\right)$
9 8 adantl ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left({C}\in {A}\wedge {C}\ne {B}\right)$
10 eldifsn ${⊢}{C}\in \left({A}\setminus \left\{{B}\right\}\right)↔\left({C}\in {A}\wedge {C}\ne {B}\right)$
11 9 10 sylibr ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to {C}\in \left({A}\setminus \left\{{B}\right\}\right)$
12 hashdifsn ${⊢}\left({A}\setminus \left\{{B}\right\}\in \mathrm{Fin}\wedge {C}\in \left({A}\setminus \left\{{B}\right\}\right)\right)\to \left|\left({A}\setminus \left\{{B}\right\}\right)\setminus \left\{{C}\right\}\right|=\left|{A}\setminus \left\{{B}\right\}\right|-1$
13 4 11 12 syl2an2r ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|\left({A}\setminus \left\{{B}\right\}\right)\setminus \left\{{C}\right\}\right|=\left|{A}\setminus \left\{{B}\right\}\right|-1$
14 hashdifsn ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in {A}\right)\to \left|{A}\setminus \left\{{B}\right\}\right|=\left|{A}\right|-1$
15 14 3ad2antr1 ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|{A}\setminus \left\{{B}\right\}\right|=\left|{A}\right|-1$
16 15 oveq1d ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|{A}\setminus \left\{{B}\right\}\right|-1=\left|{A}\right|-1-1$
17 hashcl ${⊢}{A}\in \mathrm{Fin}\to \left|{A}\right|\in {ℕ}_{0}$
18 17 nn0cnd ${⊢}{A}\in \mathrm{Fin}\to \left|{A}\right|\in ℂ$
19 sub1m1 ${⊢}\left|{A}\right|\in ℂ\to \left|{A}\right|-1-1=\left|{A}\right|-2$
20 18 19 syl ${⊢}{A}\in \mathrm{Fin}\to \left|{A}\right|-1-1=\left|{A}\right|-2$
21 20 adantr ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|{A}\right|-1-1=\left|{A}\right|-2$
22 16 21 eqtrd ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|{A}\setminus \left\{{B}\right\}\right|-1=\left|{A}\right|-2$
23 3 13 22 3eqtrd ${⊢}\left({A}\in \mathrm{Fin}\wedge \left({B}\in {A}\wedge {C}\in {A}\wedge {B}\ne {C}\right)\right)\to \left|{A}\setminus \left\{{B},{C}\right\}\right|=\left|{A}\right|-2$