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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 diffi ⊢ ( 𝐵 ∈ Fin → ( 𝐵 ∖ 𝐴 ) ∈ Fin )
2 1 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐵 ∖ 𝐴 ) ∈ Fin )
3 simpl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
4 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
5 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
6 3 4 5 sylancl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
7 sslin ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 → ( ( 𝐵 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) )
8 4 7 ax-mp ⊢ ( ( 𝐵 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 )
9 incom ⊢ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) )
10 disjdif ⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
11 9 10 eqtri ⊢ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅
12 sseq0 ⊢ ( ( ( ( 𝐵 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) ∧ ( ( 𝐵 ∖ 𝐴 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝐵 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝐵 ) ) = ∅ )
13 8 11 12 mp2an ⊢ ( ( 𝐵 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝐵 ) ) = ∅
14 13 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( 𝐵 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝐵 ) ) = ∅ )
15 hashun ⊢ ( ( ( 𝐵 ∖ 𝐴 ) ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) ∈ Fin ∧ ( ( 𝐵 ∖ 𝐴 ) ∩ ( 𝐴 ∩ 𝐵 ) ) = ∅ ) → ( ♯ ‘ ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) + ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
16 2 6 14 15 syl3anc ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) + ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
17 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
18 17 uneq2i ⊢ ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐵 ∩ 𝐴 ) )
19 uncom ⊢ ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐵 ∩ 𝐴 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) )
20 inundif ⊢ ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
21 18 19 20 3eqtri ⊢ ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝐵 ) ) = 𝐵
22 21 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝐵 ) ) = 𝐵 )
23 22 fveq2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( ( 𝐵 ∖ 𝐴 ) ∪ ( 𝐴 ∩ 𝐵 ) ) ) = ( ♯ ‘ 𝐵 ) )
24 16 23 eqtr3d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) + ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ( ♯ ‘ 𝐵 ) )
25 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
26 25 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
27 26 nn0cnd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
28 hashcl ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ Fin → ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℕ0 )
29 6 28 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℕ0 )
30 29 nn0cnd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℂ )
31 hashcl ⊢ ( ( 𝐵 ∖ 𝐴 ) ∈ Fin → ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ℕ0 )
32 2 31 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ℕ0 )
33 32 nn0cnd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ℂ )
34 27 30 33 subadd2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ↔ ( ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) + ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ( ♯ ‘ 𝐵 ) ) )
35 24 34 mpbird ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) )
36 35 oveq2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
37 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
38 37 adantr ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
39 38 nn0cnd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
40 39 27 30 addsubassd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
41 undif2 ⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 )
42 41 fveq2i ⊢ ( ♯ ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) )
43 10 a1i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
44 hashun ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐵 ∖ 𝐴 ) ∈ Fin ∧ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
45 3 2 43 44 syl3anc ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
46 42 45 eqtr3id ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
47 36 40 46 3eqtr4rd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) − ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )