Proof of Theorem hashxpe
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | 
| 2 |  | hashxp 14474 | . . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ×
𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) | 
| 3 | 1, 2 | syl 17 | . . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) | 
| 4 |  | nn0ssre 12532 | . . . . . . 7
⊢
ℕ0 ⊆ ℝ | 
| 5 |  | hashcl 14396 | . . . . . . 7
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) | 
| 6 | 4, 5 | sselid 3980 | . . . . . 6
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℝ) | 
| 7 |  | hashcl 14396 | . . . . . . 7
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) | 
| 8 | 4, 7 | sselid 3980 | . . . . . 6
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℝ) | 
| 9 | 6, 8 | anim12i 613 | . . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ∈
ℝ ∧ (♯‘𝐵) ∈ ℝ)) | 
| 10 | 1, 9 | syl 17 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → ((♯‘𝐴) ∈ ℝ ∧
(♯‘𝐵) ∈
ℝ)) | 
| 11 |  | rexmul 13314 | . . . 4
⊢
(((♯‘𝐴)
∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) →
((♯‘𝐴)
·e (♯‘𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) | 
| 12 | 10, 11 | syl 17 | . . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → ((♯‘𝐴) ·e
(♯‘𝐵)) =
((♯‘𝐴) ·
(♯‘𝐵))) | 
| 13 | 3, 12 | eqtr4d 2779 | . 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 14 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → 𝐵 = ∅) | 
| 15 | 14 | xpeq2d 5714 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (𝐴 × 𝐵) = (𝐴 × ∅)) | 
| 16 |  | xp0 6177 | . . . . . . . . 9
⊢ (𝐴 × ∅) =
∅ | 
| 17 | 15, 16 | eqtrdi 2792 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅) | 
| 18 | 17 | fveq2d 6909 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (♯‘(𝐴 × 𝐵)) =
(♯‘∅)) | 
| 19 |  | hash0 14407 | . . . . . . 7
⊢
(♯‘∅) = 0 | 
| 20 | 18, 19 | eqtrdi 2792 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (♯‘(𝐴 × 𝐵)) = 0) | 
| 21 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑉) | 
| 22 |  | hashinf 14375 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) | 
| 23 | 21, 22 | sylan 580 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (♯‘𝐴) = +∞) | 
| 25 | 14 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (♯‘𝐵) =
(♯‘∅)) | 
| 26 | 25, 19 | eqtrdi 2792 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (♯‘𝐵) = 0) | 
| 27 | 24, 26 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → ((♯‘𝐴) ·e
(♯‘𝐵)) =
(+∞ ·e 0)) | 
| 28 |  | pnfxr 11316 | . . . . . . . 8
⊢ +∞
∈ ℝ* | 
| 29 |  | xmul01 13310 | . . . . . . . 8
⊢ (+∞
∈ ℝ* → (+∞ ·e 0) =
0) | 
| 30 | 28, 29 | ax-mp 5 | . . . . . . 7
⊢ (+∞
·e 0) = 0 | 
| 31 | 27, 30 | eqtrdi 2792 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → ((♯‘𝐴) ·e
(♯‘𝐵)) =
0) | 
| 32 | 20, 31 | eqtr4d 2779 | . . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 = ∅) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 33 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ 𝑊) | 
| 34 | 33 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → 𝐵 ∈ 𝑊) | 
| 35 |  | hashxrcl 14397 | . . . . . . . 8
⊢ (𝐵 ∈ 𝑊 → (♯‘𝐵) ∈
ℝ*) | 
| 36 | 34, 35 | syl 17 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → (♯‘𝐵) ∈
ℝ*) | 
| 37 |  | hashgt0 14428 | . . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 0 <
(♯‘𝐵)) | 
| 38 | 34, 37 | sylancom 588 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → 0 <
(♯‘𝐵)) | 
| 39 |  | xmulpnf2 13318 | . . . . . . 7
⊢
(((♯‘𝐵)
∈ ℝ* ∧ 0 < (♯‘𝐵)) → (+∞ ·e
(♯‘𝐵)) =
+∞) | 
| 40 | 36, 38, 39 | syl2anc 584 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → (+∞
·e (♯‘𝐵)) = +∞) | 
| 41 | 23 | adantr 480 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → (♯‘𝐴) = +∞) | 
| 42 | 41 | oveq1d 7447 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → ((♯‘𝐴) ·e
(♯‘𝐵)) =
(+∞ ·e (♯‘𝐵))) | 
| 43 | 21 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → 𝐴 ∈ 𝑉) | 
| 44 | 43, 34 | xpexd 7772 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → (𝐴 × 𝐵) ∈ V) | 
| 45 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → ¬ 𝐴 ∈ Fin) | 
| 46 |  | 0fi 9083 | . . . . . . . . . . . 12
⊢ ∅
∈ Fin | 
| 47 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝐴 = ∅ → (𝐴 ∈ Fin ↔ ∅
∈ Fin)) | 
| 48 | 46, 47 | mpbiri 258 | . . . . . . . . . . 11
⊢ (𝐴 = ∅ → 𝐴 ∈ Fin) | 
| 49 | 48 | necon3bi 2966 | . . . . . . . . . 10
⊢ (¬
𝐴 ∈ Fin → 𝐴 ≠ ∅) | 
| 50 | 45, 49 | syl 17 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → 𝐴 ≠ ∅) | 
| 51 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → 𝐵 ≠ ∅) | 
| 52 |  | ioran 985 | . . . . . . . . . . 11
⊢ (¬
(𝐴 = ∅ ∨ 𝐵 = ∅) ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) | 
| 53 |  | xpeq0 6179 | . . . . . . . . . . . 12
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) | 
| 54 | 53 | necon3abii 2986 | . . . . . . . . . . 11
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 = ∅ ∨ 𝐵 = ∅)) | 
| 55 |  | df-ne 2940 | . . . . . . . . . . . 12
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) | 
| 56 |  | df-ne 2940 | . . . . . . . . . . . 12
⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅) | 
| 57 | 55, 56 | anbi12i 628 | . . . . . . . . . . 11
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (¬
𝐴 = ∅ ∧ ¬
𝐵 =
∅)) | 
| 58 | 52, 54, 57 | 3bitr4i 303 | . . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅)) | 
| 59 | 58 | biimpri 228 | . . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅) | 
| 60 | 50, 51, 59 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅) | 
| 61 | 45 | intnanrd 489 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | 
| 62 |  | pm4.61 404 | . . . . . . . . 9
⊢ (¬
((𝐴 × 𝐵) ≠ ∅ → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) ↔ ((𝐴 × 𝐵) ≠ ∅ ∧ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))) | 
| 63 |  | xpfir 9301 | . . . . . . . . . . 11
⊢ (((𝐴 × 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | 
| 64 | 63 | ex 412 | . . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ∈ Fin → ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))) | 
| 65 | 64 | con3i 154 | . . . . . . . . 9
⊢ (¬
((𝐴 × 𝐵) ≠ ∅ → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → ¬
(𝐴 × 𝐵) ∈ Fin) | 
| 66 | 62, 65 | sylbir 235 | . . . . . . . 8
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → ¬
(𝐴 × 𝐵) ∈ Fin) | 
| 67 | 60, 61, 66 | syl2anc 584 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → ¬ (𝐴 × 𝐵) ∈ Fin) | 
| 68 |  | hashinf 14375 | . . . . . . 7
⊢ (((𝐴 × 𝐵) ∈ V ∧ ¬ (𝐴 × 𝐵) ∈ Fin) → (♯‘(𝐴 × 𝐵)) = +∞) | 
| 69 | 44, 67, 68 | syl2anc 584 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → (♯‘(𝐴 × 𝐵)) = +∞) | 
| 70 | 40, 42, 69 | 3eqtr4rd 2787 | . . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) ∧ 𝐵 ≠ ∅) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 71 |  | exmidne 2949 | . . . . . 6
⊢ (𝐵 = ∅ ∨ 𝐵 ≠ ∅) | 
| 72 | 71 | a1i 11 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) → (𝐵 = ∅ ∨ 𝐵 ≠ ∅)) | 
| 73 | 32, 70, 72 | mpjaodan 960 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 74 | 73 | adantlr 715 | . . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) ∧ ¬ 𝐴 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 75 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → 𝐴 = ∅) | 
| 76 | 75 | xpeq1d 5713 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (𝐴 × 𝐵) = (∅ × 𝐵)) | 
| 77 |  | 0xp 5783 | . . . . . . . . 9
⊢ (∅
× 𝐵) =
∅ | 
| 78 | 76, 77 | eqtrdi 2792 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (𝐴 × 𝐵) = ∅) | 
| 79 | 78 | fveq2d 6909 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (♯‘(𝐴 × 𝐵)) =
(♯‘∅)) | 
| 80 | 79, 19 | eqtrdi 2792 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (♯‘(𝐴 × 𝐵)) = 0) | 
| 81 | 75 | fveq2d 6909 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (♯‘𝐴) =
(♯‘∅)) | 
| 82 | 81, 19 | eqtrdi 2792 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (♯‘𝐴) = 0) | 
| 83 |  | hashinf 14375 | . . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞) | 
| 84 | 33, 83 | sylan 580 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞) | 
| 85 | 84 | adantr 480 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (♯‘𝐵) = +∞) | 
| 86 | 82, 85 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → ((♯‘𝐴) ·e
(♯‘𝐵)) = (0
·e +∞)) | 
| 87 |  | xmul02 13311 | . . . . . . . 8
⊢ (+∞
∈ ℝ* → (0 ·e +∞) =
0) | 
| 88 | 28, 87 | ax-mp 5 | . . . . . . 7
⊢ (0
·e +∞) = 0 | 
| 89 | 86, 88 | eqtrdi 2792 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → ((♯‘𝐴) ·e
(♯‘𝐵)) =
0) | 
| 90 | 80, 89 | eqtr4d 2779 | . . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 = ∅) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 91 |  | hashxrcl 14397 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈
ℝ*) | 
| 92 | 91 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → (♯‘𝐴) ∈
ℝ*) | 
| 93 |  | hashgt0 14428 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 0 <
(♯‘𝐴)) | 
| 94 | 93 | ad4ant14 752 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → 0 <
(♯‘𝐴)) | 
| 95 |  | xmulpnf1 13317 | . . . . . . 7
⊢
(((♯‘𝐴)
∈ ℝ* ∧ 0 < (♯‘𝐴)) → ((♯‘𝐴) ·e +∞) =
+∞) | 
| 96 | 92, 94, 95 | syl2anc 584 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → ((♯‘𝐴) ·e +∞)
= +∞) | 
| 97 | 84 | adantr 480 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → (♯‘𝐵) = +∞) | 
| 98 | 97 | oveq2d 7448 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → ((♯‘𝐴) ·e
(♯‘𝐵)) =
((♯‘𝐴)
·e +∞)) | 
| 99 | 21 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ 𝑉) | 
| 100 | 33 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → 𝐵 ∈ 𝑊) | 
| 101 | 99, 100 | xpexd 7772 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → (𝐴 × 𝐵) ∈ V) | 
| 102 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) | 
| 103 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → ¬ 𝐵 ∈ Fin) | 
| 104 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝐵 = ∅ → (𝐵 ∈ Fin ↔ ∅
∈ Fin)) | 
| 105 | 46, 104 | mpbiri 258 | . . . . . . . . . . 11
⊢ (𝐵 = ∅ → 𝐵 ∈ Fin) | 
| 106 | 105 | necon3bi 2966 | . . . . . . . . . 10
⊢ (¬
𝐵 ∈ Fin → 𝐵 ≠ ∅) | 
| 107 | 103, 106 | syl 17 | . . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) | 
| 108 | 102, 107,
59 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅) | 
| 109 | 103 | intnand 488 | . . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | 
| 110 | 108, 109,
66 | syl2anc 584 | . . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → ¬ (𝐴 × 𝐵) ∈ Fin) | 
| 111 | 101, 110,
68 | syl2anc 584 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → (♯‘(𝐴 × 𝐵)) = +∞) | 
| 112 | 96, 98, 111 | 3eqtr4rd 2787 | . . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) ∧ 𝐴 ≠ ∅) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 113 |  | exmidne 2949 | . . . . . 6
⊢ (𝐴 = ∅ ∨ 𝐴 ≠ ∅) | 
| 114 | 113 | a1i 11 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) → (𝐴 = ∅ ∨ 𝐴 ≠ ∅)) | 
| 115 | 90, 112, 114 | mpjaodan 960 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 116 | 115 | adantlr 715 | . . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) ∧ ¬ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 117 |  | simpr 484 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | 
| 118 |  | ianor 983 | . . . 4
⊢ (¬
(𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ↔ (¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin)) | 
| 119 | 117, 118 | sylib 218 | . . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → (¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin)) | 
| 120 | 74, 116, 119 | mpjaodan 960 | . 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | 
| 121 |  | exmidd 895 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∨ ¬ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))) | 
| 122 | 13, 120, 121 | mpjaodan 960 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) |