Step | Hyp | Ref
| Expression |
1 | | fprodss.1 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
2 | | sseq2 3992 |
. . . . 5
⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅)) |
3 | | ss0 4351 |
. . . . 5
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
4 | 2, 3 | syl6bi 255 |
. . . 4
⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅)) |
5 | | prodeq1 15262 |
. . . . . 6
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ ∅ 𝐶) |
6 | | prodeq1 15262 |
. . . . . . 7
⊢ (𝐵 = ∅ → ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑘 ∈ ∅ 𝐶) |
7 | 6 | eqcomd 2827 |
. . . . . 6
⊢ (𝐵 = ∅ → ∏𝑘 ∈ ∅ 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
8 | 5, 7 | sylan9eq 2876 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
9 | 8 | expcom 416 |
. . . 4
⊢ (𝐵 = ∅ → (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
10 | 4, 9 | syld 47 |
. . 3
⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
11 | 1, 10 | syl5com 31 |
. 2
⊢ (𝜑 → (𝐵 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
12 | | cnvimass 5948 |
. . . . . . . . 9
⊢ (◡𝑓 “ 𝐴) ⊆ dom 𝑓 |
13 | | simprr 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵) |
14 | | f1of 6614 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))⟶𝐵) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))⟶𝐵) |
16 | 12, 15 | fssdm 6529 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (◡𝑓 “ 𝐴) ⊆ (1...(♯‘𝐵))) |
17 | | f1ofn 6615 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓 Fn (1...(♯‘𝐵))) |
18 | | elpreima 6827 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn (1...(♯‘𝐵)) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴))) |
19 | 13, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴))) |
20 | 15 | ffvelrnda 6850 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓‘𝑛) ∈ 𝐵) |
21 | 20 | ex 415 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (1...(♯‘𝐵)) → (𝑓‘𝑛) ∈ 𝐵)) |
22 | 21 | adantrd 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ((𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴) → (𝑓‘𝑛) ∈ 𝐵)) |
23 | 19, 22 | sylbid 242 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (◡𝑓 “ 𝐴) → (𝑓‘𝑛) ∈ 𝐵)) |
24 | 23 | imp 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (◡𝑓 “ 𝐴)) → (𝑓‘𝑛) ∈ 𝐵) |
25 | | fprodss.2 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
26 | 25 | ex 415 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
27 | 26 | adantr 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
28 | | eldif 3945 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐵 ∖ 𝐴) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) |
29 | | fprodss.3 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 1) |
30 | | ax-1cn 10594 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
31 | 29, 30 | eqeltrdi 2921 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ) |
32 | 28, 31 | sylan2br 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → 𝐶 ∈ ℂ) |
33 | 32 | expr 459 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
34 | 27, 33 | pm2.61d 181 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
35 | 34 | adantlr 713 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
36 | 35 | fmpttd 6878 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ) |
37 | 36 | ffvelrnda 6850 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ) |
38 | 24, 37 | syldan 593 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (◡𝑓 “ 𝐴)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ) |
39 | | eqid 2821 |
. . . . . . . . 9
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
40 | | simprl 769 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (♯‘𝐵) ∈
ℕ) |
41 | | nnuz 12280 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
42 | 40, 41 | eleqtrdi 2923 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (♯‘𝐵) ∈
(ℤ≥‘1)) |
43 | | ssidd 3989 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) →
(1...(♯‘𝐵))
⊆ (1...(♯‘𝐵))) |
44 | 39, 42, 43 | fprodntriv 15295 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∃𝑚 ∈
(ℤ≥‘1)∃𝑦(𝑦 ≠ 0 ∧ seq𝑚( · , (𝑛 ∈ (ℤ≥‘1)
↦ if(𝑛 ∈
(1...(♯‘𝐵)),
((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)), 1))) ⇝ 𝑦)) |
45 | | eldifi 4102 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
((1...(♯‘𝐵))
∖ (◡𝑓 “ 𝐴)) → 𝑛 ∈ (1...(♯‘𝐵))) |
46 | 45, 20 | sylan2 594 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ 𝐵) |
47 | | eldifn 4103 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
((1...(♯‘𝐵))
∖ (◡𝑓 “ 𝐴)) → ¬ 𝑛 ∈ (◡𝑓 “ 𝐴)) |
48 | 47 | adantl 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ¬ 𝑛 ∈ (◡𝑓 “ 𝐴)) |
49 | 45 | adantl 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → 𝑛 ∈ (1...(♯‘𝐵))) |
50 | 19 | adantr 483 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴))) |
51 | 49, 50 | mpbirand 705 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑓‘𝑛) ∈ 𝐴)) |
52 | 48, 51 | mtbid 326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ¬ (𝑓‘𝑛) ∈ 𝐴) |
53 | 46, 52 | eldifd 3946 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴)) |
54 | | difss 4107 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵 |
55 | | resmpt 5904 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∖ 𝐴) ⊆ 𝐵 → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶) |
57 | 56 | fveq1i 6670 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) |
58 | | fvres 6688 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
59 | 57, 58 | syl5eqr 2870 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
60 | 53, 59 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
61 | | 1ex 10636 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
62 | 61 | elsn2 4603 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ {1} ↔ 𝐶 = 1) |
63 | 29, 62 | sylibr 236 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ {1}) |
64 | 63 | fmpttd 6878 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{1}) |
65 | 64 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{1}) |
66 | 65, 53 | ffvelrnd 6851 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {1}) |
67 | | elsni 4583 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {1} → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 1) |
68 | 66, 67 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 1) |
69 | 60, 68 | eqtr3d 2858 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = 1) |
70 | | fzssuz 12947 |
. . . . . . . . 9
⊢
(1...(♯‘𝐵)) ⊆
(ℤ≥‘1) |
71 | 70 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) →
(1...(♯‘𝐵))
⊆ (ℤ≥‘1)) |
72 | 16, 38, 44, 69, 71 | prodss 15300 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∏𝑛 ∈ (◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = ∏𝑛 ∈ (1...(♯‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
73 | 1 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝐴 ⊆ 𝐵) |
74 | 73 | resmptd 5907 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴) = (𝑘 ∈ 𝐴 ↦ 𝐶)) |
75 | 74 | fveq1d 6671 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) |
76 | | fvres 6688 |
. . . . . . . . . 10
⊢ (𝑚 ∈ 𝐴 → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
77 | 75, 76 | sylan9req 2877 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
78 | 77 | prodeq2dv 15276 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
79 | | fveq2 6669 |
. . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
80 | | fzfid 13340 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) →
(1...(♯‘𝐵))
∈ Fin) |
81 | 80, 15 | fisuppfi 8840 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (◡𝑓 “ 𝐴) ∈ Fin) |
82 | | f1of1 6613 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))–1-1→𝐵) |
83 | 13, 82 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1→𝐵) |
84 | | f1ores 6628 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝐵))–1-1→𝐵 ∧ (◡𝑓 “ 𝐴) ⊆ (1...(♯‘𝐵))) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (◡𝑓 “ 𝐴))) |
85 | 83, 16, 84 | syl2anc 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (◡𝑓 “ 𝐴))) |
86 | | f1ofo 6621 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))–onto→𝐵) |
87 | 13, 86 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–onto→𝐵) |
88 | | foimacnv 6631 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...(♯‘𝐵))–onto→𝐵 ∧ 𝐴 ⊆ 𝐵) → (𝑓 “ (◡𝑓 “ 𝐴)) = 𝐴) |
89 | 87, 73, 88 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 “ (◡𝑓 “ 𝐴)) = 𝐴) |
90 | 89 | f1oeq3d 6611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ((𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (◡𝑓 “ 𝐴)) ↔ (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→𝐴)) |
91 | 85, 90 | mpbid 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→𝐴) |
92 | | fvres 6688 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (◡𝑓 “ 𝐴) → ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛)) |
93 | 92 | adantl 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (◡𝑓 “ 𝐴)) → ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛)) |
94 | 73 | sselda 3966 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐵) |
95 | 36 | ffvelrnda 6850 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ) |
96 | 94, 95 | syldan 593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ) |
97 | 79, 81, 91, 93, 96 | fprodf1o 15299 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ∏𝑛 ∈ (◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
98 | 78, 97 | eqtrd 2856 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑛 ∈ (◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
99 | | eqidd 2822 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓‘𝑛) = (𝑓‘𝑛)) |
100 | 79, 80, 13, 99, 95 | fprodf1o 15299 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ∏𝑛 ∈ (1...(♯‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
101 | 72, 98, 100 | 3eqtr4d 2866 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
102 | | prodfc 15298 |
. . . . . 6
⊢
∏𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐶 |
103 | | prodfc 15298 |
. . . . . 6
⊢
∏𝑚 ∈
𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐵 𝐶 |
104 | 101, 102,
103 | 3eqtr3g 2879 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
105 | 104 | expr 459 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
106 | 105 | exlimdv 1930 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
107 | 106 | expimpd 456 |
. 2
⊢ (𝜑 → (((♯‘𝐵) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
108 | | fprodss.4 |
. . 3
⊢ (𝜑 → 𝐵 ∈ Fin) |
109 | | fz1f1o 15066 |
. . 3
⊢ (𝐵 ∈ Fin → (𝐵 = ∅ ∨
((♯‘𝐵) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵))) |
110 | 108, 109 | syl 17 |
. 2
⊢ (𝜑 → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵))) |
111 | 11, 107, 110 | mpjaod 856 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |