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		0fin	⊢ ∅ ∈ 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 ( ♯ ‘ 𝐵 ) ) )