This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashxpe

Description: The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023)

Ref Expression
Assertion hashxpe ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )
2 hashxp ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )
3 1 2 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )
4 nn0ssre ⊢ ℕ0 ⊆ ℝ
5 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
6 4 5 sselid ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℝ )
7 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
8 4 7 sselid ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℝ )
9 6 8 anim12i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) )
10 1 9 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) )
11 rexmul ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )
12 10 11 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )
13 3 12 eqtr4d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
14 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
15 14 xpeq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
16 xp0 ⊢ ( 𝐴 × ∅ ) = ∅
17 15 16 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( 𝐴 × 𝐵 ) = ∅ )
18 17 fveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ♯ ‘ ∅ ) )
19 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
20 18 19 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = 0 )
21 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
22 hashinf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
23 21 22 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
24 23 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ♯ ‘ 𝐴 ) = +∞ )
25 14 fveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ∅ ) )
26 25 19 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ♯ ‘ 𝐵 ) = 0 )
27 24 26 oveq12d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = ( +∞ ·e 0 ) )
28 pnfxr ⊢ +∞ ∈ ℝ*
29 xmul01 ⊢ ( +∞ ∈ ℝ* → ( +∞ ·e 0 ) = 0 )
30 28 29 ax-mp ⊢ ( +∞ ·e 0 ) = 0
31 27 30 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = 0 )
32 20 31 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 = ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
33 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
34 33 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → 𝐵 ∈ 𝑊 )
35 hashxrcl ⊢ ( 𝐵 ∈ 𝑊 → ( ♯ ‘ 𝐵 ) ∈ ℝ* )
36 34 35 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℝ* )
37 hashgt0 ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐵 ) )
38 34 37 sylancom ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐵 ) )
39 xmulpnf2 ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℝ* ∧ 0 < ( ♯ ‘ 𝐵 ) ) → ( +∞ ·e ( ♯ ‘ 𝐵 ) ) = +∞ )
40 36 38 39 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( +∞ ·e ( ♯ ‘ 𝐵 ) ) = +∞ )
41 23 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) = +∞ )
42 41 oveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = ( +∞ ·e ( ♯ ‘ 𝐵 ) ) )
43 21 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → 𝐴 ∈ 𝑉 )
44 43 34 xpexd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ∈ V )
45 simplr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ¬ 𝐴 ∈ Fin )
46 0fi ⊢ ∅ ∈ Fin
47 eleq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ Fin ↔ ∅ ∈ Fin ) )
48 46 47 mpbiri ⊢ ( 𝐴 = ∅ → 𝐴 ∈ Fin )
49 48 necon3bi ⊢ ( ¬ 𝐴 ∈ Fin → 𝐴 ≠ ∅ )
50 45 49 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → 𝐴 ≠ ∅ )
51 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → 𝐵 ≠ ∅ )
52 ioran ⊢ ( ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ↔ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) )
53 xpeq0 ⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )
54 53 necon3abii ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ ↔ ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )
55 df-ne ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
56 df-ne ⊢ ( 𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅ )
57 55 56 anbi12i ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) )
58 52 54 57 3bitr4i ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ ↔ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
59 58 biimpri ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
60 50 51 59 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
61 45 intnanrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )
62 pm4.61 ⊢ ( ¬ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) ↔ ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) )
63 xpfir ⊢ ( ( ( 𝐴 × 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )
64 63 ex ⊢ ( ( 𝐴 × 𝐵 ) ∈ Fin → ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) )
65 64 con3i ⊢ ( ¬ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ¬ ( 𝐴 × 𝐵 ) ∈ Fin )
66 62 65 sylbir ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ¬ ( 𝐴 × 𝐵 ) ∈ Fin )
67 60 61 66 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ¬ ( 𝐴 × 𝐵 ) ∈ Fin )
68 hashinf ⊢ ( ( ( 𝐴 × 𝐵 ) ∈ V ∧ ¬ ( 𝐴 × 𝐵 ) ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = +∞ )
69 44 67 68 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = +∞ )
70 40 42 69 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ≠ ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
71 exmidne ⊢ ( 𝐵 = ∅ ∨ 𝐵 ≠ ∅ )
72 71 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐵 = ∅ ∨ 𝐵 ≠ ∅ ) )
73 32 70 72 mpjaodan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
74 73 adantlr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
75 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
76 75 xpeq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( 𝐴 × 𝐵 ) = ( ∅ × 𝐵 ) )
77 0xp ⊢ ( ∅ × 𝐵 ) = ∅
78 76 77 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( 𝐴 × 𝐵 ) = ∅ )
79 78 fveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ♯ ‘ ∅ ) )
80 79 19 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = 0 )
81 75 fveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) )
82 81 19 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ 𝐴 ) = 0 )
83 hashinf ⊢ ( ( 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
84 33 83 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
85 84 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ 𝐵 ) = +∞ )
86 82 85 oveq12d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = ( 0 ·e +∞ ) )
87 xmul02 ⊢ ( +∞ ∈ ℝ* → ( 0 ·e +∞ ) = 0 )
88 28 87 ax-mp ⊢ ( 0 ·e +∞ ) = 0
89 86 88 eqtrdi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = 0 )
90 80 89 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 = ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
91 hashxrcl ⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
92 91 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
93 hashgt0 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐴 ) )
94 93 ad4ant14 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐴 ) )
95 xmulpnf1 ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ* ∧ 0 < ( ♯ ‘ 𝐴 ) ) → ( ( ♯ ‘ 𝐴 ) ·e +∞ ) = +∞ )
96 92 94 95 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( ( ♯ ‘ 𝐴 ) ·e +∞ ) = +∞ )
97 84 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐵 ) = +∞ )
98 97 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e +∞ ) )
99 21 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ 𝑉 )
100 33 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ 𝑊 )
101 99 100 xpexd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ∈ V )
102 simpr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
103 simplr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ¬ 𝐵 ∈ Fin )
104 eleq1 ⊢ ( 𝐵 = ∅ → ( 𝐵 ∈ Fin ↔ ∅ ∈ Fin ) )
105 46 104 mpbiri ⊢ ( 𝐵 = ∅ → 𝐵 ∈ Fin )
106 105 necon3bi ⊢ ( ¬ 𝐵 ∈ Fin → 𝐵 ≠ ∅ )
107 103 106 syl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐵 ≠ ∅ )
108 102 107 59 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
109 103 intnand ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )
110 108 109 66 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ¬ ( 𝐴 × 𝐵 ) ∈ Fin )
111 101 110 68 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = +∞ )
112 96 98 111 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
113 exmidne ⊢ ( 𝐴 = ∅ ∨ 𝐴 ≠ ∅ )
114 113 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴 = ∅ ∨ 𝐴 ≠ ∅ ) )
115 90 112 114 mpjaodan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
116 115 adantlr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
117 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )
118 ianor ⊢ ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ↔ ( ¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin ) )
119 117 118 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ( ¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin ) )
120 74 116 119 mpjaodan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )
121 exmidd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∨ ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ) )
122 13 120 121 mpjaodan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) ·e ( ♯ ‘ 𝐵 ) ) )