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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 )