Proof of Theorem hashun3
Step | Hyp | Ref
| Expression |
1 | | diffi 8596 |
. . . . . . 7
⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin) |
2 | 1 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐵 ∖ 𝐴) ∈ Fin) |
3 | | simpl 483 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin) |
4 | | inss1 4125 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
5 | | ssfi 8584 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐴 ∩ 𝐵) ∈ Fin) |
6 | 3, 4, 5 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ 𝐵) ∈ Fin) |
7 | | sslin 4131 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴)) |
8 | 4, 7 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) |
9 | | incom 4099 |
. . . . . . . . 9
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = (𝐴 ∩ (𝐵 ∖ 𝐴)) |
10 | | disjdif 4335 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ |
11 | 9, 10 | eqtri 2819 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
12 | | sseq0 4273 |
. . . . . . . 8
⊢ ((((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) ∧ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
13 | 8, 11, 12 | mp2an 688 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅ |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
15 | | hashun 13591 |
. . . . . 6
⊢ (((𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ 𝐵) ∈ Fin ∧ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) → (♯‘((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵))) = ((♯‘(𝐵 ∖ 𝐴)) + (♯‘(𝐴 ∩ 𝐵)))) |
16 | 2, 6, 14, 15 | syl3anc 1364 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘((𝐵 ∖
𝐴) ∪ (𝐴 ∩ 𝐵))) = ((♯‘(𝐵 ∖ 𝐴)) + (♯‘(𝐴 ∩ 𝐵)))) |
17 | | incom 4099 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
18 | 17 | uneq2i 4057 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) |
19 | | uncom 4050 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) = ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) |
20 | | inundif 4341 |
. . . . . . . 8
⊢ ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
21 | 18, 19, 20 | 3eqtri 2823 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵 |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵) |
23 | 22 | fveq2d 6542 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘((𝐵 ∖
𝐴) ∪ (𝐴 ∩ 𝐵))) = (♯‘𝐵)) |
24 | 16, 23 | eqtr3d 2833 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘(𝐵 ∖
𝐴)) + (♯‘(𝐴 ∩ 𝐵))) = (♯‘𝐵)) |
25 | | hashcl 13567 |
. . . . . . 7
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
26 | 25 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐵) ∈
ℕ0) |
27 | 26 | nn0cnd 11805 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐵) ∈
ℂ) |
28 | | hashcl 13567 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ Fin → (♯‘(𝐴 ∩ 𝐵)) ∈
ℕ0) |
29 | 6, 28 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∩
𝐵)) ∈
ℕ0) |
30 | 29 | nn0cnd 11805 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∩
𝐵)) ∈
ℂ) |
31 | | hashcl 13567 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∈ Fin → (♯‘(𝐵 ∖ 𝐴)) ∈
ℕ0) |
32 | 2, 31 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐵 ∖
𝐴)) ∈
ℕ0) |
33 | 32 | nn0cnd 11805 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐵 ∖
𝐴)) ∈
ℂ) |
34 | 27, 30, 33 | subadd2d 10864 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))) =
(♯‘(𝐵 ∖
𝐴)) ↔
((♯‘(𝐵 ∖
𝐴)) + (♯‘(𝐴 ∩ 𝐵))) = (♯‘𝐵))) |
35 | 24, 34 | mpbird 258 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))) =
(♯‘(𝐵 ∖
𝐴))) |
36 | 35 | oveq2d 7032 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵)))) =
((♯‘𝐴) +
(♯‘(𝐵 ∖
𝐴)))) |
37 | | hashcl 13567 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
38 | 37 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐴) ∈
ℕ0) |
39 | 38 | nn0cnd 11805 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐴) ∈
ℂ) |
40 | 39, 27, 30 | addsubassd 10865 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘(𝐴 ∩
𝐵))) =
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))))) |
41 | | undif2 4339 |
. . . 4
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
42 | 41 | fveq2i 6541 |
. . 3
⊢
(♯‘(𝐴
∪ (𝐵 ∖ 𝐴))) = (♯‘(𝐴 ∪ 𝐵)) |
43 | 10 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) |
44 | | hashun 13591 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) → (♯‘(𝐴 ∪ (𝐵 ∖ 𝐴))) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
45 | 3, 2, 43, 44 | syl3anc 1364 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
(𝐵 ∖ 𝐴))) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
46 | 42, 45 | syl5eqr 2845 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
𝐵)) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
47 | 36, 40, 46 | 3eqtr4rd 2842 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
𝐵)) =
(((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘(𝐴 ∩
𝐵)))) |