Metamath Proof Explorer

Theorem hashun3

Description: The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017)

Ref Expression
Assertion hashun3 
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( ( # ` A ) + ( # ` B ) ) - ( # ` ( A i^i B ) ) ) )

Proof

Step Hyp Ref Expression
1 diffi 
 |-  ( B e. Fin -> ( B \ A ) e. Fin )
2 1 adantl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( B \ A ) e. Fin )
3 simpl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> A e. Fin )
4 inss1 
 |-  ( A i^i B ) C_ A
5 ssfi 
 |-  ( ( A e. Fin /\ ( A i^i B ) C_ A ) -> ( A i^i B ) e. Fin )
6 3 4 5 sylancl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A i^i B ) e. Fin )
7 sslin 
 |-  ( ( A i^i B ) C_ A -> ( ( B \ A ) i^i ( A i^i B ) ) C_ ( ( B \ A ) i^i A ) )
8 4 7 ax-mp 
 |-  ( ( B \ A ) i^i ( A i^i B ) ) C_ ( ( B \ A ) i^i A )
9 disjdifr 
 |-  ( ( B \ A ) i^i A ) = (/)
10 sseq0 
 |-  ( ( ( ( B \ A ) i^i ( A i^i B ) ) C_ ( ( B \ A ) i^i A ) /\ ( ( B \ A ) i^i A ) = (/) ) -> ( ( B \ A ) i^i ( A i^i B ) ) = (/) )
11 8 9 10 mp2an 
 |-  ( ( B \ A ) i^i ( A i^i B ) ) = (/)
12 11 a1i 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( B \ A ) i^i ( A i^i B ) ) = (/) )
13 hashun 
 |-  ( ( ( B \ A ) e. Fin /\ ( A i^i B ) e. Fin /\ ( ( B \ A ) i^i ( A i^i B ) ) = (/) ) -> ( # ` ( ( B \ A ) u. ( A i^i B ) ) ) = ( ( # ` ( B \ A ) ) + ( # ` ( A i^i B ) ) ) )
14 2 6 12 13 syl3anc 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( ( B \ A ) u. ( A i^i B ) ) ) = ( ( # ` ( B \ A ) ) + ( # ` ( A i^i B ) ) ) )
15 incom 
 |-  ( A i^i B ) = ( B i^i A )
16 15 uneq2i 
 |-  ( ( B \ A ) u. ( A i^i B ) ) = ( ( B \ A ) u. ( B i^i A ) )
17 uncom 
 |-  ( ( B \ A ) u. ( B i^i A ) ) = ( ( B i^i A ) u. ( B \ A ) )
18 inundif 
 |-  ( ( B i^i A ) u. ( B \ A ) ) = B
19 16 17 18 3eqtri 
 |-  ( ( B \ A ) u. ( A i^i B ) ) = B
20 19 a1i 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( B \ A ) u. ( A i^i B ) ) = B )
21 20 fveq2d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( ( B \ A ) u. ( A i^i B ) ) ) = ( # ` B ) )
22 14 21 eqtr3d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` ( B \ A ) ) + ( # ` ( A i^i B ) ) ) = ( # ` B ) )
23 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
24 23 adantl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` B ) e. NN0 )
25 24 nn0cnd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` B ) e. CC )
26 hashcl 
 |-  ( ( A i^i B ) e. Fin -> ( # ` ( A i^i B ) ) e. NN0 )
27 6 26 syl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A i^i B ) ) e. NN0 )
28 27 nn0cnd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A i^i B ) ) e. CC )
29 hashcl 
 |-  ( ( B \ A ) e. Fin -> ( # ` ( B \ A ) ) e. NN0 )
30 2 29 syl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( B \ A ) ) e. NN0 )
31 30 nn0cnd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( B \ A ) ) e. CC )
32 25 28 31 subadd2d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( ( # ` B ) - ( # ` ( A i^i B ) ) ) = ( # ` ( B \ A ) ) <-> ( ( # ` ( B \ A ) ) + ( # ` ( A i^i B ) ) ) = ( # ` B ) ) )
33 22 32 mpbird 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` B ) - ( # ` ( A i^i B ) ) ) = ( # ` ( B \ A ) ) )
34 33 oveq2d 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) + ( ( # ` B ) - ( # ` ( A i^i B ) ) ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) )
35 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
36 35 adantr 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` A ) e. NN0 )
37 36 nn0cnd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` A ) e. CC )
38 37 25 28 addsubassd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( ( # ` A ) + ( # ` B ) ) - ( # ` ( A i^i B ) ) ) = ( ( # ` A ) + ( ( # ` B ) - ( # ` ( A i^i B ) ) ) ) )
39 undif2 
 |-  ( A u. ( B \ A ) ) = ( A u. B )
40 39 fveq2i 
 |-  ( # ` ( A u. ( B \ A ) ) ) = ( # ` ( A u. B ) )
41 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
42 41 a1i 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A i^i ( B \ A ) ) = (/) )
43 hashun 
 |-  ( ( A e. Fin /\ ( B \ A ) e. Fin /\ ( A i^i ( B \ A ) ) = (/) ) -> ( # ` ( A u. ( B \ A ) ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) )
44 3 2 42 43 syl3anc 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. ( B \ A ) ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) )
45 40 44 eqtr3id 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( # ` A ) + ( # ` ( B \ A ) ) ) )
46 34 38 45 3eqtr4rd 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A u. B ) ) = ( ( ( # ` A ) + ( # ` B ) ) - ( # ` ( A i^i B ) ) ) )