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