Metamath Proof Explorer

Theorem hashdifpr

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

Ref Expression
Assertion hashdifpr ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖BC=A−2

Proof

Step Hyp Ref Expression
1 difpr ⊢A∖BC=A∖B∖C
2 1 a1i ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖BC=A∖B∖C
3 2 fveq2d ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖BC=A∖B∖C
4 diffi ⊢A∈Fin→A∖B∈Fin
5 necom ⊢B≠C↔C≠B
6 5 biimpi ⊢B≠C→C≠B
7 6 anim2i ⊢C∈A∧B≠C→C∈A∧C≠B
8 7 3adant1 ⊢B∈A∧C∈A∧B≠C→C∈A∧C≠B
9 8 adantl ⊢A∈Fin∧B∈A∧C∈A∧B≠C→C∈A∧C≠B
10 eldifsn ⊢C∈A∖B↔C∈A∧C≠B
11 9 10 sylibr ⊢A∈Fin∧B∈A∧C∈A∧B≠C→C∈A∖B
12 hashdifsn ⊢A∖B∈Fin∧C∈A∖B→A∖B∖C=A∖B−1
13 4 11 12 syl2an2r ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖B∖C=A∖B−1
14 hashdifsn ⊢A∈Fin∧B∈A→A∖B=A−1
15 14 3ad2antr1 ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖B=A−1
16 15 oveq1d ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖B−1=A-1-1
17 hashcl ⊢A∈Fin→A∈ℕ0
18 17 nn0cnd ⊢A∈Fin→A∈ℂ
19 sub1m1 ⊢A∈ℂ→A-1-1=A−2
20 18 19 syl ⊢A∈Fin→A-1-1=A−2
21 20 adantr ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A-1-1=A−2
22 16 21 eqtrd ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖B−1=A−2
23 3 13 22 3eqtrd ⊢A∈Fin∧B∈A∧C∈A∧B≠C→A∖BC=A−2