Proof of Theorem hashun3
Step | Hyp | Ref
| Expression |
1 | | diffi 8738 |
. . . . . . 7
⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin) |
2 | 1 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐵 ∖ 𝐴) ∈ Fin) |
3 | | simpl 483 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin) |
4 | | inss1 4202 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
5 | | ssfi 8726 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐴 ∩ 𝐵) ∈ Fin) |
6 | 3, 4, 5 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ 𝐵) ∈ Fin) |
7 | | sslin 4208 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴)) |
8 | 4, 7 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) |
9 | | incom 4175 |
. . . . . . . . 9
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = (𝐴 ∩ (𝐵 ∖ 𝐴)) |
10 | | disjdif 4417 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ |
11 | 9, 10 | eqtri 2841 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
12 | | sseq0 4350 |
. . . . . . . 8
⊢ ((((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) ∧ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
13 | 8, 11, 12 | mp2an 688 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅ |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
15 | | hashun 13731 |
. . . . . 6
⊢ (((𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ 𝐵) ∈ Fin ∧ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) → (♯‘((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵))) = ((♯‘(𝐵 ∖ 𝐴)) + (♯‘(𝐴 ∩ 𝐵)))) |
16 | 2, 6, 14, 15 | syl3anc 1363 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘((𝐵 ∖
𝐴) ∪ (𝐴 ∩ 𝐵))) = ((♯‘(𝐵 ∖ 𝐴)) + (♯‘(𝐴 ∩ 𝐵)))) |
17 | | incom 4175 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
18 | 17 | uneq2i 4133 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) |
19 | | uncom 4126 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) = ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) |
20 | | inundif 4423 |
. . . . . . . 8
⊢ ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
21 | 18, 19, 20 | 3eqtri 2845 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵 |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵) |
23 | 22 | fveq2d 6667 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘((𝐵 ∖
𝐴) ∪ (𝐴 ∩ 𝐵))) = (♯‘𝐵)) |
24 | 16, 23 | eqtr3d 2855 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘(𝐵 ∖
𝐴)) + (♯‘(𝐴 ∩ 𝐵))) = (♯‘𝐵)) |
25 | | hashcl 13705 |
. . . . . . 7
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
26 | 25 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐵) ∈
ℕ0) |
27 | 26 | nn0cnd 11945 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐵) ∈
ℂ) |
28 | | hashcl 13705 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ Fin → (♯‘(𝐴 ∩ 𝐵)) ∈
ℕ0) |
29 | 6, 28 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∩
𝐵)) ∈
ℕ0) |
30 | 29 | nn0cnd 11945 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∩
𝐵)) ∈
ℂ) |
31 | | hashcl 13705 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∈ Fin → (♯‘(𝐵 ∖ 𝐴)) ∈
ℕ0) |
32 | 2, 31 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐵 ∖
𝐴)) ∈
ℕ0) |
33 | 32 | nn0cnd 11945 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐵 ∖
𝐴)) ∈
ℂ) |
34 | 27, 30, 33 | subadd2d 11004 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))) =
(♯‘(𝐵 ∖
𝐴)) ↔
((♯‘(𝐵 ∖
𝐴)) + (♯‘(𝐴 ∩ 𝐵))) = (♯‘𝐵))) |
35 | 24, 34 | mpbird 258 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))) =
(♯‘(𝐵 ∖
𝐴))) |
36 | 35 | oveq2d 7161 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵)))) =
((♯‘𝐴) +
(♯‘(𝐵 ∖
𝐴)))) |
37 | | hashcl 13705 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
38 | 37 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐴) ∈
ℕ0) |
39 | 38 | nn0cnd 11945 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐴) ∈
ℂ) |
40 | 39, 27, 30 | addsubassd 11005 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘(𝐴 ∩
𝐵))) =
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))))) |
41 | | undif2 4421 |
. . . 4
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
42 | 41 | fveq2i 6666 |
. . 3
⊢
(♯‘(𝐴
∪ (𝐵 ∖ 𝐴))) = (♯‘(𝐴 ∪ 𝐵)) |
43 | 10 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) |
44 | | hashun 13731 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) → (♯‘(𝐴 ∪ (𝐵 ∖ 𝐴))) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
45 | 3, 2, 43, 44 | syl3anc 1363 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
(𝐵 ∖ 𝐴))) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
46 | 42, 45 | syl5eqr 2867 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
𝐵)) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
47 | 36, 40, 46 | 3eqtr4rd 2864 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
𝐵)) =
(((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘(𝐴 ∩
𝐵)))) |