Proof of Theorem hashunx
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hashun 14421 | . . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 2 | 1 | 3expa 1119 | . . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 3 |  | hashcl 14395 | . . . . . . . . . 10
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) | 
| 4 | 3 | nn0red 12588 | . . . . . . . . 9
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℝ) | 
| 5 |  | hashcl 14395 | . . . . . . . . . 10
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) | 
| 6 | 5 | nn0red 12588 | . . . . . . . . 9
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℝ) | 
| 7 | 4, 6 | anim12i 613 | . . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ∈
ℝ ∧ (♯‘𝐵) ∈ ℝ)) | 
| 8 | 7 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((♯‘𝐴) ∈ ℝ ∧
(♯‘𝐵) ∈
ℝ)) | 
| 9 |  | rexadd 13274 | . . . . . . 7
⊢
(((♯‘𝐴)
∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) →
((♯‘𝐴)
+𝑒 (♯‘𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 10 | 8, 9 | syl 17 | . . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((♯‘𝐴) +𝑒
(♯‘𝐵)) =
((♯‘𝐴) +
(♯‘𝐵))) | 
| 11 | 10 | eqcomd 2743 | . . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → ((♯‘𝐴) + (♯‘𝐵)) = ((♯‘𝐴) +𝑒
(♯‘𝐵))) | 
| 12 | 2, 11 | eqtrd 2777 | . . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵))) | 
| 13 | 12 | expcom 413 | . . 3
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵)))) | 
| 14 | 13 | 3ad2ant3 1136 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵)))) | 
| 15 |  | unexg 7763 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | 
| 16 |  | unfir 9346 | . . . . . . 7
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | 
| 17 | 16 | con3i 154 | . . . . . 6
⊢ (¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∪ 𝐵) ∈ Fin) | 
| 18 |  | hashinf 14374 | . . . . . 6
⊢ (((𝐴 ∪ 𝐵) ∈ V ∧ ¬ (𝐴 ∪ 𝐵) ∈ Fin) → (♯‘(𝐴 ∪ 𝐵)) = +∞) | 
| 19 | 15, 17, 18 | syl2anr 597 | . . . . 5
⊢ ((¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (♯‘(𝐴 ∪ 𝐵)) = +∞) | 
| 20 |  | ianor 984 | . . . . . . 7
⊢ (¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ↔ (¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin)) | 
| 21 |  | simprl 771 | . . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐴 ∈ 𝑉) | 
| 22 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐵 ∈ 𝑊) | 
| 23 |  | hashnfinnn0 14400 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) ∉
ℕ0) | 
| 24 | 23 | ex 412 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ Fin → (♯‘𝐴) ∉
ℕ0)) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝐴 ∈ Fin → (♯‘𝐴) ∉
ℕ0)) | 
| 26 | 25 | impcom 407 | . . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (♯‘𝐴) ∉
ℕ0) | 
| 27 |  | hashinfxadd 14424 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (♯‘𝐴) ∉ ℕ0) →
((♯‘𝐴)
+𝑒 (♯‘𝐵)) = +∞) | 
| 28 | 21, 22, 26, 27 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((♯‘𝐴) +𝑒 (♯‘𝐵)) = +∞) | 
| 29 | 28 | eqcomd 2743 | . . . . . . . . 9
⊢ ((¬
𝐴 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → +∞ = ((♯‘𝐴) +𝑒
(♯‘𝐵))) | 
| 30 | 29 | ex 412 | . . . . . . . 8
⊢ (¬
𝐴 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((♯‘𝐴) +𝑒
(♯‘𝐵)))) | 
| 31 |  | hashxrcl 14396 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈
ℝ*) | 
| 32 |  | hashxrcl 14396 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑊 → (♯‘𝐵) ∈
ℝ*) | 
| 33 | 31, 32 | anim12i 613 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((♯‘𝐴) ∈ ℝ* ∧
(♯‘𝐵) ∈
ℝ*)) | 
| 34 | 33 | adantl 481 | . . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((♯‘𝐴) ∈ ℝ* ∧
(♯‘𝐵) ∈
ℝ*)) | 
| 35 |  | xaddcom 13282 | . . . . . . . . . . . 12
⊢
(((♯‘𝐴)
∈ ℝ* ∧ (♯‘𝐵) ∈ ℝ*) →
((♯‘𝐴)
+𝑒 (♯‘𝐵)) = ((♯‘𝐵) +𝑒 (♯‘𝐴))) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . . 11
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((♯‘𝐴) +𝑒 (♯‘𝐵)) = ((♯‘𝐵) +𝑒
(♯‘𝐴))) | 
| 37 |  | simprr 773 | . . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐵 ∈ 𝑊) | 
| 38 |  | simprl 771 | . . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → 𝐴 ∈ 𝑉) | 
| 39 |  | hashnfinnn0 14400 | . . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) ∉
ℕ0) | 
| 40 | 39 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑊 → (¬ 𝐵 ∈ Fin → (♯‘𝐵) ∉
ℕ0)) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝐵 ∈ Fin → (♯‘𝐵) ∉
ℕ0)) | 
| 42 | 41 | impcom 407 | . . . . . . . . . . . 12
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (♯‘𝐵) ∉
ℕ0) | 
| 43 |  | hashinfxadd 14424 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ (♯‘𝐵) ∉ ℕ0) →
((♯‘𝐵)
+𝑒 (♯‘𝐴)) = +∞) | 
| 44 | 37, 38, 42, 43 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((♯‘𝐵) +𝑒 (♯‘𝐴)) = +∞) | 
| 45 | 36, 44 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → ((♯‘𝐴) +𝑒 (♯‘𝐵)) = +∞) | 
| 46 | 45 | eqcomd 2743 | . . . . . . . . 9
⊢ ((¬
𝐵 ∈ Fin ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → +∞ = ((♯‘𝐴) +𝑒
(♯‘𝐵))) | 
| 47 | 46 | ex 412 | . . . . . . . 8
⊢ (¬
𝐵 ∈ Fin → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((♯‘𝐴) +𝑒
(♯‘𝐵)))) | 
| 48 | 30, 47 | jaoi 858 | . . . . . . 7
⊢ ((¬
𝐴 ∈ Fin ∨ ¬
𝐵 ∈ Fin) →
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((♯‘𝐴) +𝑒
(♯‘𝐵)))) | 
| 49 | 20, 48 | sylbi 217 | . . . . . 6
⊢ (¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → +∞ = ((♯‘𝐴) +𝑒
(♯‘𝐵)))) | 
| 50 | 49 | imp 406 | . . . . 5
⊢ ((¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → +∞ = ((♯‘𝐴) +𝑒
(♯‘𝐵))) | 
| 51 | 19, 50 | eqtrd 2777 | . . . 4
⊢ ((¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵))) | 
| 52 | 51 | expcom 413 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵)))) | 
| 53 | 52 | 3adant3 1133 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ∪
𝐵)) = ((♯‘𝐴) +𝑒
(♯‘𝐵)))) | 
| 54 | 14, 53 | pm2.61d 179 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵))) |