Theorem fprodf1o

Description: Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017)

	Ref	Expression
Hypotheses	fprodf1o.1	⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
	fprodf1o.2	⊢ ( 𝜑 → 𝐶 ∈ Fin )
	fprodf1o.3	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
	fprodf1o.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
	fprodf1o.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	fprodf1o	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fprodf1o.1	⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
2		fprodf1o.2	⊢ ( 𝜑 → 𝐶 ∈ Fin )
3		fprodf1o.3	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
4		fprodf1o.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
5		fprodf1o.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6		prod0	⊢ ∏ 𝑘 ∈ ∅ 𝐵 = 1
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
8		f1oeq2	⊢ ( 𝐶 = ∅ → ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 ↔ 𝐹 : ∅ –1-1-onto→ 𝐴 ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 ↔ 𝐹 : ∅ –1-1-onto→ 𝐴 ) )
10	7 9	mpbid	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐹 : ∅ –1-1-onto→ 𝐴 )
11		f1ofo	⊢ ( 𝐹 : ∅ –1-1-onto→ 𝐴 → 𝐹 : ∅ –onto→ 𝐴 )
12	10 11	syl	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐹 : ∅ –onto→ 𝐴 )
13		fo00	⊢ ( 𝐹 : ∅ –onto→ 𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
14	13	simprbi	⊢ ( 𝐹 : ∅ –onto→ 𝐴 → 𝐴 = ∅ )
15	12 14	syl	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐴 = ∅ )
16	15	prodeq1d	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
17		prodeq1	⊢ ( 𝐶 = ∅ → ∏ 𝑛 ∈ 𝐶 𝐷 = ∏ 𝑛 ∈ ∅ 𝐷 )
18		prod0	⊢ ∏ 𝑛 ∈ ∅ 𝐷 = 1
19	17 18	eqtrdi	⊢ ( 𝐶 = ∅ → ∏ 𝑛 ∈ 𝐶 𝐷 = 1 )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → ∏ 𝑛 ∈ 𝐶 𝐷 = 1 )
21	6 16 20	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 )
22	21	ex	⊢ ( 𝜑 → ( 𝐶 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 ) )
23		2fveq3	⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
24		simprl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℕ )
25		simprr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 )
26		f1of	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 ⟶ 𝐴 )
27	3 26	syl	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐴 )
28	27	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 )
29	5	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
30	29	ffvelcdmda	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
31	28 30	syldan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
32	31	adantlr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
33		simpr	⊢ ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 )
34		f1oco	⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐴 )
35	3 33 34	syl2an	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐴 )
36		f1of	⊢ ( ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐴 → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
37	35 36	syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
38		fvco3	⊢ ( ( ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) )
39	37 38	sylan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) )
40		f1of	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
41	40	adantl	⊢ ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
42	41	adantl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
43		fvco3	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) )
44	42 43	sylan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) )
45	44	fveq2d	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
46	39 45	eqtrd	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
47	23 24 25 32 46	fprod	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ∏ 𝑚 ∈ 𝐶 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) = ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
48	27	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 )
49	4 48	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐺 ∈ 𝐴 )
50		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
51	1 50	fvmpti	⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
52	49 51	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
53	4	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐺 ) )
54		eqid	⊢ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑛 ∈ 𝐶 ↦ 𝐷 )
55	54	fvmpt2i	⊢ ( 𝑛 ∈ 𝐶 → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
56	55	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
57	52 53 56	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) )
58	57	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) )
59		nffvmpt1	⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 )
60	59	nfeq1	⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) )
61		fveq2	⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) )
62		2fveq3	⊢ ( 𝑛 = 𝑚 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
63	61 62	eqeq12d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
64	60 63	rspc	⊢ ( 𝑚 ∈ 𝐶 → ( ∀ 𝑛 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
65	58 64	mpan9	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
66	65	adantlr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
67	66	prodeq2dv	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ∏ 𝑚 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ∏ 𝑚 ∈ 𝐶 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
68		fveq2	⊢ ( 𝑚 = ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) )
69	29	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
70	69	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
71	68 24 35 70 39	fprod	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
72	47 67 71	3eqtr4rd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ∏ 𝑚 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) )
73		prodfc	⊢ ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝐴 𝐵
74		prodfc	⊢ ∏ 𝑚 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ∏ 𝑛 ∈ 𝐶 𝐷
75	72 73 74	3eqtr3g	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 )
76	75	expr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 ) )
77	76	exlimdv	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 ) )
78	77	expimpd	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 ) )
79		fz1f1o	⊢ ( 𝐶 ∈ Fin → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) )
80	2 79	syl	⊢ ( 𝜑 → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) )
81	22 78 80	mpjaod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 )