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
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ) |
29 |
5
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ) |
30 |
29
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ ) |
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
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) |
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
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 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 |
⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑛 ∈ 𝐶 𝐷 ) |