Proof of Theorem hashun3
Step | Hyp | Ref
| Expression |
1 | | diffi 8906 |
. . . . . . 7
⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin) |
2 | 1 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐵 ∖ 𝐴) ∈ Fin) |
3 | | simpl 486 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin) |
4 | | inss1 4143 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
5 | | ssfi 8851 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐴 ∩ 𝐵) ∈ Fin) |
6 | 3, 4, 5 | sylancl 589 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ 𝐵) ∈ Fin) |
7 | | sslin 4149 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴)) |
8 | 4, 7 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) |
9 | | disjdifr 4387 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
10 | | sseq0 4314 |
. . . . . . . 8
⊢ ((((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) ⊆ ((𝐵 ∖ 𝐴) ∩ 𝐴) ∧ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
11 | 8, 9, 10 | mp2an 692 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅ |
12 | 11 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) |
13 | | hashun 13949 |
. . . . . 6
⊢ (((𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ 𝐵) ∈ Fin ∧ ((𝐵 ∖ 𝐴) ∩ (𝐴 ∩ 𝐵)) = ∅) → (♯‘((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵))) = ((♯‘(𝐵 ∖ 𝐴)) + (♯‘(𝐴 ∩ 𝐵)))) |
14 | 2, 6, 12, 13 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘((𝐵 ∖
𝐴) ∪ (𝐴 ∩ 𝐵))) = ((♯‘(𝐵 ∖ 𝐴)) + (♯‘(𝐴 ∩ 𝐵)))) |
15 | | incom 4115 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
16 | 15 | uneq2i 4074 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) |
17 | | uncom 4067 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐵 ∩ 𝐴)) = ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) |
18 | | inundif 4393 |
. . . . . . . 8
⊢ ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
19 | 16, 17, 18 | 3eqtri 2769 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵 |
20 | 19 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐵 ∖ 𝐴) ∪ (𝐴 ∩ 𝐵)) = 𝐵) |
21 | 20 | fveq2d 6721 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘((𝐵 ∖
𝐴) ∪ (𝐴 ∩ 𝐵))) = (♯‘𝐵)) |
22 | 14, 21 | eqtr3d 2779 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘(𝐵 ∖
𝐴)) + (♯‘(𝐴 ∩ 𝐵))) = (♯‘𝐵)) |
23 | | hashcl 13923 |
. . . . . . 7
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
24 | 23 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐵) ∈
ℕ0) |
25 | 24 | nn0cnd 12152 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐵) ∈
ℂ) |
26 | | hashcl 13923 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ Fin → (♯‘(𝐴 ∩ 𝐵)) ∈
ℕ0) |
27 | 6, 26 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∩
𝐵)) ∈
ℕ0) |
28 | 27 | nn0cnd 12152 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∩
𝐵)) ∈
ℂ) |
29 | | hashcl 13923 |
. . . . . . 7
⊢ ((𝐵 ∖ 𝐴) ∈ Fin → (♯‘(𝐵 ∖ 𝐴)) ∈
ℕ0) |
30 | 2, 29 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐵 ∖
𝐴)) ∈
ℕ0) |
31 | 30 | nn0cnd 12152 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐵 ∖
𝐴)) ∈
ℂ) |
32 | 25, 28, 31 | subadd2d 11208 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))) =
(♯‘(𝐵 ∖
𝐴)) ↔
((♯‘(𝐵 ∖
𝐴)) + (♯‘(𝐴 ∩ 𝐵))) = (♯‘𝐵))) |
33 | 22, 32 | mpbird 260 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))) =
(♯‘(𝐵 ∖
𝐴))) |
34 | 33 | oveq2d 7229 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵)))) =
((♯‘𝐴) +
(♯‘(𝐵 ∖
𝐴)))) |
35 | | hashcl 13923 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
36 | 35 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐴) ∈
ℕ0) |
37 | 36 | nn0cnd 12152 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘𝐴) ∈
ℂ) |
38 | 37, 25, 28 | addsubassd 11209 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘(𝐴 ∩
𝐵))) =
((♯‘𝐴) +
((♯‘𝐵) −
(♯‘(𝐴 ∩
𝐵))))) |
39 | | undif2 4391 |
. . . 4
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
40 | 39 | fveq2i 6720 |
. . 3
⊢
(♯‘(𝐴
∪ (𝐵 ∖ 𝐴))) = (♯‘(𝐴 ∪ 𝐵)) |
41 | | disjdif 4386 |
. . . . 5
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ |
42 | 41 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) |
43 | | hashun 13949 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin ∧ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅) → (♯‘(𝐴 ∪ (𝐵 ∖ 𝐴))) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
44 | 3, 2, 42, 43 | syl3anc 1373 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
(𝐵 ∖ 𝐴))) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
45 | 40, 44 | eqtr3id 2792 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
𝐵)) = ((♯‘𝐴) + (♯‘(𝐵 ∖ 𝐴)))) |
46 | 34, 38, 45 | 3eqtr4rd 2788 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
𝐵)) =
(((♯‘𝐴) +
(♯‘𝐵)) −
(♯‘(𝐴 ∩
𝐵)))) |