Proof of Theorem hashunx
Step | Hyp | Ref
| Expression |
1 | | hashun 13032 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
2 | 1 | 3expa 1257 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
3 | | hashcl 13009 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
4 | 3 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℝ) |
5 | | hashcl 13009 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin →
(#‘𝐵) ∈
ℕ0) |
6 | 5 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝐵 ∈ Fin →
(#‘𝐵) ∈
ℝ) |
7 | 4, 6 | anim12i 588 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐴) ∈ ℝ
∧ (#‘𝐵) ∈
ℝ)) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((#‘𝐴) ∈ ℝ ∧
(#‘𝐵) ∈
ℝ)) |
9 | | rexadd 11937 |
. . . . . . 7
⊢
(((#‘𝐴) ∈
ℝ ∧ (#‘𝐵)
∈ ℝ) → ((#‘𝐴) +𝑒 (#‘𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((#‘𝐴) +𝑒
(#‘𝐵)) =
((#‘𝐴) +
(#‘𝐵))) |
11 | 10 | eqcomd 2616 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((#‘𝐴) + (#‘𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵))) |
12 | 2, 11 | eqtrd 2644 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵))) |
13 | 12 | expcom 450 |
. . 3
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵)))) |
14 | 13 | 3ad2ant3 1077 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵)))) |
15 | | unexg 6857 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
16 | | unfir 8113 |
. . . . . . 7
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) |
17 | 16 | con3i 149 |
. . . . . 6
⊢ (¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∪ 𝐵) ∈ Fin) |
18 | | hashinf 12984 |
. . . . . 6
⊢ (((𝐴 ∪ 𝐵) ∈ V ∧ ¬ (𝐴 ∪ 𝐵) ∈ Fin) → (#‘(𝐴 ∪ 𝐵)) = +∞) |
19 | 15, 17, 18 | syl2anr 494 |
. . . . 5
⊢ ((¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (#‘(𝐴 ∪ 𝐵)) = +∞) |
20 | | ianor 508 |
. . . . . . 7
⊢ (¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ↔ (¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin)) |
21 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐴 ∈ 𝑉) |
22 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐵 ∈ 𝑊) |
23 | | hashnfinnn0 13013 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (#‘𝐴) ∉
ℕ0) |
24 | 23 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ Fin → (#‘𝐴) ∉
ℕ0)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝐴 ∈ Fin → (#‘𝐴) ∉
ℕ0)) |
26 | 25 | impcom 445 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (#‘𝐴) ∉
ℕ0) |
27 | | hashinfxadd 13035 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (#‘𝐴) ∉ ℕ0) →
((#‘𝐴)
+𝑒 (#‘𝐵)) = +∞) |
28 | 21, 22, 26, 27 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((#‘𝐴) +𝑒 (#‘𝐵)) = +∞) |
29 | 28 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → +∞ = ((#‘𝐴) +𝑒
(#‘𝐵))) |
30 | 29 | ex 449 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((#‘𝐴) +𝑒
(#‘𝐵)))) |
31 | | hashxrcl 13010 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → (#‘𝐴) ∈
ℝ*) |
32 | | hashxrcl 13010 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑊 → (#‘𝐵) ∈
ℝ*) |
33 | 31, 32 | anim12i 588 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((#‘𝐴) ∈ ℝ* ∧
(#‘𝐵) ∈
ℝ*)) |
34 | 33 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((#‘𝐴) ∈ ℝ* ∧
(#‘𝐵) ∈
ℝ*)) |
35 | | xaddcom 11945 |
. . . . . . . . . . . 12
⊢
(((#‘𝐴) ∈
ℝ* ∧ (#‘𝐵) ∈ ℝ*) →
((#‘𝐴)
+𝑒 (#‘𝐵)) = ((#‘𝐵) +𝑒 (#‘𝐴))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((#‘𝐴) +𝑒 (#‘𝐵)) = ((#‘𝐵) +𝑒 (#‘𝐴))) |
37 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐵 ∈ 𝑊) |
38 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐴 ∈ 𝑉) |
39 | | hashnfinnn0 13013 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐵) ∉
ℕ0) |
40 | 39 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑊 → (¬ 𝐵 ∈ Fin → (#‘𝐵) ∉
ℕ0)) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝐵 ∈ Fin → (#‘𝐵) ∉
ℕ0)) |
42 | 41 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (#‘𝐵) ∉
ℕ0) |
43 | | hashinfxadd 13035 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ (#‘𝐵) ∉ ℕ0) →
((#‘𝐵)
+𝑒 (#‘𝐴)) = +∞) |
44 | 37, 38, 42, 43 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((#‘𝐵) +𝑒 (#‘𝐴)) = +∞) |
45 | 36, 44 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((#‘𝐴) +𝑒 (#‘𝐵)) = +∞) |
46 | 45 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → +∞ = ((#‘𝐴) +𝑒
(#‘𝐵))) |
47 | 46 | ex 449 |
. . . . . . . 8
⊢ (¬
𝐵 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((#‘𝐴) +𝑒
(#‘𝐵)))) |
48 | 30, 47 | jaoi 393 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ Fin ∨ ¬
𝐵 ∈ Fin) →
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((#‘𝐴) +𝑒
(#‘𝐵)))) |
49 | 20, 48 | sylbi 206 |
. . . . . 6
⊢ (¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((#‘𝐴) +𝑒
(#‘𝐵)))) |
50 | 49 | imp 444 |
. . . . 5
⊢ ((¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → +∞ = ((#‘𝐴) +𝑒
(#‘𝐵))) |
51 | 19, 50 | eqtrd 2644 |
. . . 4
⊢ ((¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵))) |
52 | 51 | expcom 450 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵)))) |
53 | 52 | 3adant3 1074 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵)))) |
54 | 14, 53 | pm2.61d 169 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵))) |