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 e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( # ` ( A \ { B , C } ) ) = ( ( # ` A ) - 2 ) )

Proof

Step Hyp Ref Expression
1 difpr
 |-  ( A \ { B , C } ) = ( ( A \ { B } ) \ { C } )
2 1 a1i
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( A \ { B , C } ) = ( ( A \ { B } ) \ { C } ) )
3 2 fveq2d
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( # ` ( A \ { B , C } ) ) = ( # ` ( ( A \ { B } ) \ { C } ) ) )
4 diffi
 |-  ( A e. Fin -> ( A \ { B } ) e. Fin )
5 necom
 |-  ( B =/= C <-> C =/= B )
6 5 biimpi
 |-  ( B =/= C -> C =/= B )
7 6 anim2i
 |-  ( ( C e. A /\ B =/= C ) -> ( C e. A /\ C =/= B ) )
8 7 3adant1
 |-  ( ( B e. A /\ C e. A /\ B =/= C ) -> ( C e. A /\ C =/= B ) )
9 8 adantl
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( C e. A /\ C =/= B ) )
10 eldifsn
 |-  ( C e. ( A \ { B } ) <-> ( C e. A /\ C =/= B ) )
11 9 10 sylibr
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> C e. ( A \ { B } ) )
12 hashdifsn
 |-  ( ( ( A \ { B } ) e. Fin /\ C e. ( A \ { B } ) ) -> ( # ` ( ( A \ { B } ) \ { C } ) ) = ( ( # ` ( A \ { B } ) ) - 1 ) )
13 4 11 12 syl2an2r
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( # ` ( ( A \ { B } ) \ { C } ) ) = ( ( # ` ( A \ { B } ) ) - 1 ) )
14 hashdifsn
 |-  ( ( A e. Fin /\ B e. A ) -> ( # ` ( A \ { B } ) ) = ( ( # ` A ) - 1 ) )
15 14 3ad2antr1
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( # ` ( A \ { B } ) ) = ( ( # ` A ) - 1 ) )
16 15 oveq1d
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( ( # ` ( A \ { B } ) ) - 1 ) = ( ( ( # ` A ) - 1 ) - 1 ) )
17 hashcl
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
18 17 nn0cnd
 |-  ( A e. Fin -> ( # ` A ) e. CC )
19 sub1m1
 |-  ( ( # ` A ) e. CC -> ( ( ( # ` A ) - 1 ) - 1 ) = ( ( # ` A ) - 2 ) )
20 18 19 syl
 |-  ( A e. Fin -> ( ( ( # ` A ) - 1 ) - 1 ) = ( ( # ` A ) - 2 ) )
21 20 adantr
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( ( ( # ` A ) - 1 ) - 1 ) = ( ( # ` A ) - 2 ) )
22 16 21 eqtrd
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( ( # ` ( A \ { B } ) ) - 1 ) = ( ( # ` A ) - 2 ) )
23 3 13 22 3eqtrd
 |-  ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( # ` ( A \ { B , C } ) ) = ( ( # ` A ) - 2 ) )