Metamath Proof Explorer

Theorem hashssdif

Description: The size of the difference of a finite set and a subset is the set's size minus the subset's. (Contributed by Steve Rodriguez, 24-Oct-2015)

Ref Expression
Assertion hashssdif 
|- ( ( A e. Fin /\ B C_ A ) -> ( # ` ( A \ B ) ) = ( ( # ` A ) - ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 ssfi 
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
2 diffi 
 |-  ( A e. Fin -> ( A \ B ) e. Fin )
3 disjdif 
 |-  ( B i^i ( A \ B ) ) = (/)
4 hashun 
 |-  ( ( B e. Fin /\ ( A \ B ) e. Fin /\ ( B i^i ( A \ B ) ) = (/) ) -> ( # ` ( B u. ( A \ B ) ) ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) )
5 3 4 mp3an3 
 |-  ( ( B e. Fin /\ ( A \ B ) e. Fin ) -> ( # ` ( B u. ( A \ B ) ) ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) )
6 1 2 5 syl2an 
 |-  ( ( ( A e. Fin /\ B C_ A ) /\ A e. Fin ) -> ( # ` ( B u. ( A \ B ) ) ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) )
7 6 anabss1 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( # ` ( B u. ( A \ B ) ) ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) )
8 undif 
 |-  ( B C_ A <-> ( B u. ( A \ B ) ) = A )
9 8 biimpi 
 |-  ( B C_ A -> ( B u. ( A \ B ) ) = A )
10 9 fveqeq2d 
 |-  ( B C_ A -> ( ( # ` ( B u. ( A \ B ) ) ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) <-> ( # ` A ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) ) )
11 10 adantl 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( ( # ` ( B u. ( A \ B ) ) ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) <-> ( # ` A ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) ) )
12 7 11 mpbid 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( # ` A ) = ( ( # ` B ) + ( # ` ( A \ B ) ) ) )
13 12 eqcomd 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( ( # ` B ) + ( # ` ( A \ B ) ) ) = ( # ` A ) )
14 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
15 14 nn0cnd 
 |-  ( A e. Fin -> ( # ` A ) e. CC )
16 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
17 1 16 syl 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( # ` B ) e. NN0 )
18 17 nn0cnd 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( # ` B ) e. CC )
19 hashcl 
 |-  ( ( A \ B ) e. Fin -> ( # ` ( A \ B ) ) e. NN0 )
20 2 19 syl 
 |-  ( A e. Fin -> ( # ` ( A \ B ) ) e. NN0 )
21 20 nn0cnd 
 |-  ( A e. Fin -> ( # ` ( A \ B ) ) e. CC )
22 subadd 
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC /\ ( # ` ( A \ B ) ) e. CC ) -> ( ( ( # ` A ) - ( # ` B ) ) = ( # ` ( A \ B ) ) <-> ( ( # ` B ) + ( # ` ( A \ B ) ) ) = ( # ` A ) ) )
23 15 18 21 22 syl3an 
 |-  ( ( A e. Fin /\ ( A e. Fin /\ B C_ A ) /\ A e. Fin ) -> ( ( ( # ` A ) - ( # ` B ) ) = ( # ` ( A \ B ) ) <-> ( ( # ` B ) + ( # ` ( A \ B ) ) ) = ( # ` A ) ) )
24 23 3anidm13 
 |-  ( ( A e. Fin /\ ( A e. Fin /\ B C_ A ) ) -> ( ( ( # ` A ) - ( # ` B ) ) = ( # ` ( A \ B ) ) <-> ( ( # ` B ) + ( # ` ( A \ B ) ) ) = ( # ` A ) ) )
25 24 anabss5 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( ( ( # ` A ) - ( # ` B ) ) = ( # ` ( A \ B ) ) <-> ( ( # ` B ) + ( # ` ( A \ B ) ) ) = ( # ` A ) ) )
26 13 25 mpbird 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( ( # ` A ) - ( # ` B ) ) = ( # ` ( A \ B ) ) )
27 26 eqcomd 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( # ` ( A \ B ) ) = ( ( # ` A ) - ( # ` B ) ) )