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