Proof of Theorem hashun3
Step | Hyp | Ref
| Expression |
1 | | diffi 8077 |
. . . . . . 7
⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin) |
2 | 1 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐵 ∖ 𝐴) ∈ Fin) |
3 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin) |
4 | | inss1 3795 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
5 | | ssfi 8065 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐴 ∩ 𝐵) ∈ Fin) |
6 | 3, 4, 5 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ 𝐵) ∈ Fin) |
7 | | sslin 3801 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴)) |
8 | 4, 7 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) |
9 | | incom 3767 |
. . . . . . . . 9
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = (𝐴 ∩ (𝐵 ∖ 𝐴)) |
10 | | disjdif 3992 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ |
11 | 9, 10 | eqtri 2632 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
12 | | sseq0 3927 |
. . . . . . . 8
⊢ ((((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) ∧ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
13 | 8, 11, 12 | mp2an 704 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅ |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
15 | | hashun 13032 |
. . . . . 6
⊢ (((𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ 𝐵) ∈ Fin ∧ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) → (#‘((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵))) = ((#‘(𝐵 ∖ 𝐴)) + (#‘(𝐴 ∩ 𝐵)))) |
16 | 2, 6, 14, 15 | syl3anc 1318 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵))) = ((#‘(𝐵 ∖ 𝐴)) + (#‘(𝐴 ∩ 𝐵)))) |
17 | | incom 3767 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
18 | 17 | uneq2i 3726 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) |
19 | | uncom 3719 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) = ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) |
20 | | inundif 3998 |
. . . . . . . 8
⊢ ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
21 | 18, 19, 20 | 3eqtri 2636 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵 |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵) |
23 | 22 | fveq2d 6107 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵))) = (#‘𝐵)) |
24 | 16, 23 | eqtr3d 2646 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘(𝐵 ∖ 𝐴)) + (#‘(𝐴 ∩ 𝐵))) = (#‘𝐵)) |
25 | | hashcl 13009 |
. . . . . . 7
⊢ (𝐵 ∈ Fin →
(#‘𝐵) ∈
ℕ0) |
26 | 25 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘𝐵) ∈
ℕ0) |
27 | 26 | nn0cnd 11230 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘𝐵) ∈
ℂ) |
28 | | hashcl 13009 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ Fin → (#‘(𝐴 ∩ 𝐵)) ∈
ℕ0) |
29 | 6, 28 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐴 ∩ 𝐵)) ∈
ℕ0) |
30 | 29 | nn0cnd 11230 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐴 ∩ 𝐵)) ∈
ℂ) |
31 | | hashcl 13009 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∈ Fin → (#‘(𝐵 ∖ 𝐴)) ∈
ℕ0) |
32 | 2, 31 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐵 ∖ 𝐴)) ∈
ℕ0) |
33 | 32 | nn0cnd 11230 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐵 ∖ 𝐴)) ∈
ℂ) |
34 | 27, 30, 33 | subadd2d 10290 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((#‘𝐵) −
(#‘(𝐴 ∩ 𝐵))) = (#‘(𝐵 ∖ 𝐴)) ↔ ((#‘(𝐵 ∖ 𝐴)) + (#‘(𝐴 ∩ 𝐵))) = (#‘𝐵))) |
35 | 24, 34 | mpbird 246 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐵) −
(#‘(𝐴 ∩ 𝐵))) = (#‘(𝐵 ∖ 𝐴))) |
36 | 35 | oveq2d 6565 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐴) +
((#‘𝐵) −
(#‘(𝐴 ∩ 𝐵)))) = ((#‘𝐴) + (#‘(𝐵 ∖ 𝐴)))) |
37 | | hashcl 13009 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
38 | 37 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘𝐴) ∈
ℕ0) |
39 | 38 | nn0cnd 11230 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘𝐴) ∈
ℂ) |
40 | 39, 27, 30 | addsubassd 10291 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((#‘𝐴) +
(#‘𝐵)) −
(#‘(𝐴 ∩ 𝐵))) = ((#‘𝐴) + ((#‘𝐵) − (#‘(𝐴 ∩ 𝐵))))) |
41 | | undif2 3996 |
. . . 4
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
42 | 41 | fveq2i 6106 |
. . 3
⊢
(#‘(𝐴 ∪
(𝐵 ∖ 𝐴))) = (#‘(𝐴 ∪ 𝐵)) |
43 | 10 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) |
44 | | hashun 13032 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) → (#‘(𝐴 ∪ (𝐵 ∖ 𝐴))) = ((#‘𝐴) + (#‘(𝐵 ∖ 𝐴)))) |
45 | 3, 2, 43, 44 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐴 ∪ (𝐵 ∖ 𝐴))) = ((#‘𝐴) + (#‘(𝐵 ∖ 𝐴)))) |
46 | 42, 45 | syl5eqr 2658 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) + (#‘(𝐵 ∖ 𝐴)))) |
47 | 36, 40, 46 | 3eqtr4rd 2655 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐴 ∪ 𝐵)) = (((#‘𝐴) + (#‘𝐵)) − (#‘(𝐴 ∩ 𝐵)))) |