Step | Hyp | Ref
| Expression |
1 | | fprodss.1 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
2 | | sseq2 3590 |
. . . . 5
⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅)) |
3 | | ss0 3926 |
. . . . 5
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
4 | 2, 3 | syl6bi 242 |
. . . 4
⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅)) |
5 | | prodeq1 14478 |
. . . . . 6
⊢ (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ ∅ 𝐶) |
6 | | prodeq1 14478 |
. . . . . . 7
⊢ (𝐵 = ∅ → ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑘 ∈ ∅ 𝐶) |
7 | 6 | eqcomd 2616 |
. . . . . 6
⊢ (𝐵 = ∅ → ∏𝑘 ∈ ∅ 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
8 | 5, 7 | sylan9eq 2664 |
. . . . 5
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
9 | 8 | expcom 450 |
. . . 4
⊢ (𝐵 = ∅ → (𝐴 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
10 | 4, 9 | syld 46 |
. . 3
⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
11 | 1, 10 | syl5com 31 |
. 2
⊢ (𝜑 → (𝐵 = ∅ → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
12 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡𝑓 “ 𝐴) ⊆ dom 𝑓 |
13 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵) |
14 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(#‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(#‘𝐵))⟶𝐵) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(#‘𝐵))⟶𝐵) |
16 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝐵))⟶𝐵 → dom 𝑓 = (1...(#‘𝐵))) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → dom 𝑓 = (1...(#‘𝐵))) |
18 | 12, 17 | syl5sseq 3616 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (◡𝑓 “ 𝐴) ⊆ (1...(#‘𝐵))) |
19 | | f1ofn 6051 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(#‘𝐵))–1-1-onto→𝐵 → 𝑓 Fn (1...(#‘𝐵))) |
20 | 13, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → 𝑓 Fn (1...(#‘𝐵))) |
21 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn (1...(#‘𝐵)) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(#‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(#‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴))) |
23 | 15 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (1...(#‘𝐵))) → (𝑓‘𝑛) ∈ 𝐵) |
24 | 23 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (1...(#‘𝐵)) → (𝑓‘𝑛) ∈ 𝐵)) |
25 | 24 | adantrd 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ((𝑛 ∈ (1...(#‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴) → (𝑓‘𝑛) ∈ 𝐵)) |
26 | 22, 25 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (◡𝑓 “ 𝐴) → (𝑓‘𝑛) ∈ 𝐵)) |
27 | 26 | imp 444 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (◡𝑓 “ 𝐴)) → (𝑓‘𝑛) ∈ 𝐵) |
28 | | fprodss.2 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
31 | | eldif 3550 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐵 ∖ 𝐴) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) |
32 | | fprodss.3 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 1) |
33 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
34 | 32, 33 | syl6eqel 2696 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ) |
35 | 31, 34 | sylan2br 492 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → 𝐶 ∈ ℂ) |
36 | 35 | expr 641 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
37 | 30, 36 | pm2.61d 169 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
38 | 37 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
39 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶) |
40 | 38, 39 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ) |
41 | 40 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ) |
42 | 27, 41 | syldan 486 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (◡𝑓 “ 𝐴)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ) |
43 | | eqid 2610 |
. . . . . . . . 9
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
44 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (#‘𝐵) ∈
ℕ) |
45 | | nnuz 11599 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
46 | 44, 45 | syl6eleq 2698 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (#‘𝐵) ∈
(ℤ≥‘1)) |
47 | | ssid 3587 |
. . . . . . . . . 10
⊢
(1...(#‘𝐵))
⊆ (1...(#‘𝐵)) |
48 | 47 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (1...(#‘𝐵)) ⊆ (1...(#‘𝐵))) |
49 | 43, 46, 48 | fprodntriv 14511 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∃𝑚 ∈
(ℤ≥‘1)∃𝑦(𝑦 ≠ 0 ∧ seq𝑚( · , (𝑛 ∈ (ℤ≥‘1)
↦ if(𝑛 ∈
(1...(#‘𝐵)), ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)), 1))) ⇝ 𝑦)) |
50 | | eldifi 3694 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴)) → 𝑛 ∈ (1...(#‘𝐵))) |
51 | 50, 23 | sylan2 490 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ 𝐵) |
52 | | eldifn 3695 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴)) → ¬ 𝑛 ∈ (◡𝑓 “ 𝐴)) |
53 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ¬ 𝑛 ∈ (◡𝑓 “ 𝐴)) |
54 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(#‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴))) |
55 | 50 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → 𝑛 ∈ (1...(#‘𝐵))) |
56 | 55 | biantrurd 528 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑓‘𝑛) ∈ 𝐴 ↔ (𝑛 ∈ (1...(#‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴))) |
57 | 54, 56 | bitr4d 270 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑛 ∈ (◡𝑓 “ 𝐴) ↔ (𝑓‘𝑛) ∈ 𝐴)) |
58 | 53, 57 | mtbid 313 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ¬ (𝑓‘𝑛) ∈ 𝐴) |
59 | 51, 58 | eldifd 3551 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴)) |
60 | | difss 3699 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵 |
61 | | resmpt 5369 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∖ 𝐴) ⊆ 𝐵 → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶) |
63 | 62 | fveq1i 6104 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) |
64 | | fvres 6117 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
65 | 63, 64 | syl5eqr 2658 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
66 | 59, 65 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
67 | | 1ex 9914 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
68 | 67 | elsn2 4158 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ {1} ↔ 𝐶 = 1) |
69 | 32, 68 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ {1}) |
70 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶) |
71 | 69, 70 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{1}) |
72 | 71 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{1}) |
73 | 72, 59 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {1}) |
74 | | elsni 4142 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {1} → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 1) |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 1) |
76 | 66, 75 | eqtr3d 2646 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(#‘𝐵)) ∖ (◡𝑓 “ 𝐴))) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = 1) |
77 | | fzssuz 12253 |
. . . . . . . . 9
⊢
(1...(#‘𝐵))
⊆ (ℤ≥‘1) |
78 | 77 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (1...(#‘𝐵)) ⊆
(ℤ≥‘1)) |
79 | 18, 42, 49, 76, 78 | prodss 14516 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∏𝑛 ∈ (◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = ∏𝑛 ∈ (1...(#‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
80 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → 𝐴 ⊆ 𝐵) |
81 | 80 | resmptd 5371 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴) = (𝑘 ∈ 𝐴 ↦ 𝐶)) |
82 | 81 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) |
83 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑚 ∈ 𝐴 → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
84 | 82, 83 | sylan9req 2665 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
85 | 84 | prodeq2dv 14492 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
86 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
87 | | fzfid 12634 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (1...(#‘𝐵)) ∈ Fin) |
88 | 87, 15 | fisuppfi 8166 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (◡𝑓 “ 𝐴) ∈ Fin) |
89 | | f1of1 6049 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(#‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(#‘𝐵))–1-1→𝐵) |
90 | 13, 89 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(#‘𝐵))–1-1→𝐵) |
91 | | f1ores 6064 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(#‘𝐵))–1-1→𝐵 ∧ (◡𝑓 “ 𝐴) ⊆ (1...(#‘𝐵))) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (◡𝑓 “ 𝐴))) |
92 | 90, 18, 91 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (◡𝑓 “ 𝐴))) |
93 | | f1ofo 6057 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(#‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(#‘𝐵))–onto→𝐵) |
94 | 13, 93 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(#‘𝐵))–onto→𝐵) |
95 | | foimacnv 6067 |
. . . . . . . . . . . 12
⊢ ((𝑓:(1...(#‘𝐵))–onto→𝐵 ∧ 𝐴 ⊆ 𝐵) → (𝑓 “ (◡𝑓 “ 𝐴)) = 𝐴) |
96 | 94, 80, 95 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (𝑓 “ (◡𝑓 “ 𝐴)) = 𝐴) |
97 | | f1oeq3 6042 |
. . . . . . . . . . 11
⊢ ((𝑓 “ (◡𝑓 “ 𝐴)) = 𝐴 → ((𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (◡𝑓 “ 𝐴)) ↔ (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→𝐴)) |
98 | 96, 97 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ((𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (◡𝑓 “ 𝐴)) ↔ (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→𝐴)) |
99 | 92, 98 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→𝐴) |
100 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (◡𝑓 “ 𝐴) → ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛)) |
101 | 100 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (◡𝑓 “ 𝐴)) → ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛)) |
102 | 80 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐵) |
103 | 40 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ) |
104 | 102, 103 | syldan 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ) |
105 | 86, 88, 99, 101, 104 | fprodf1o 14515 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ∏𝑛 ∈ (◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
106 | 85, 105 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑛 ∈ (◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
107 | | eqidd 2611 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (1...(#‘𝐵))) → (𝑓‘𝑛) = (𝑓‘𝑛)) |
108 | 86, 87, 13, 107, 103 | fprodf1o 14515 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ∏𝑛 ∈ (1...(#‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛))) |
109 | 79, 106, 108 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
110 | | prodfc 14514 |
. . . . . 6
⊢
∏𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐶 |
111 | | prodfc 14514 |
. . . . . 6
⊢
∏𝑚 ∈
𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐵 𝐶 |
112 | 109, 110,
111 | 3eqtr3g 2667 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝐵) ∈ ℕ ∧ 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵)) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |
113 | 112 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝐵) ∈ ℕ) → (𝑓:(1...(#‘𝐵))–1-1-onto→𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
114 | 113 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (#‘𝐵) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
115 | 114 | expimpd 627 |
. 2
⊢ (𝜑 → (((#‘𝐵) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)) |
116 | | fprodss.4 |
. . 3
⊢ (𝜑 → 𝐵 ∈ Fin) |
117 | | fz1f1o 14288 |
. . 3
⊢ (𝐵 ∈ Fin → (𝐵 = ∅ ∨ ((#‘𝐵) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵))) |
118 | 116, 117 | syl 17 |
. 2
⊢ (𝜑 → (𝐵 = ∅ ∨ ((#‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐵))–1-1-onto→𝐵))) |
119 | 11, 115, 118 | mpjaod 395 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶) |