This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )