Step | Hyp | Ref
| Expression |
1 | | ssid 3167 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
2 | | fprod2d.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
3 | | sseq1 3170 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
4 | | prodeq1 11516 |
. . . . . . 7
⊢ (𝑤 = ∅ → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶) |
5 | | iuneq1 3886 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → ∪ 𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ ∅ ({𝑗} × 𝐵)) |
6 | | 0iun 3930 |
. . . . . . . . 9
⊢ ∪ 𝑗 ∈ ∅ ({𝑗} × 𝐵) = ∅ |
7 | 5, 6 | eqtrdi 2219 |
. . . . . . . 8
⊢ (𝑤 = ∅ → ∪ 𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∅) |
8 | 7 | prodeq1d 11527 |
. . . . . . 7
⊢ (𝑤 = ∅ → ∏𝑧 ∈ ∪ 𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∅ 𝐷) |
9 | 4, 8 | eqeq12d 2185 |
. . . . . 6
⊢ (𝑤 = ∅ → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷)) |
10 | 3, 9 | imbi12d 233 |
. . . . 5
⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ (∅ ⊆ 𝐴 → ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷))) |
11 | 10 | imbi2d 229 |
. . . 4
⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → (∅ ⊆ 𝐴 → ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷)))) |
12 | | sseq1 3170 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝑤 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴)) |
13 | | prodeq1 11516 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶) |
14 | | iuneq1 3886 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)) |
15 | 14 | prodeq1d 11527 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) |
16 | 13, 15 | eqeq12d 2185 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)) |
17 | 12, 16 | imbi12d 233 |
. . . . 5
⊢ (𝑤 = 𝑥 → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ (𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷))) |
18 | 17 | imbi2d 229 |
. . . 4
⊢ (𝑤 = 𝑥 → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → (𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)))) |
19 | | sseq1 3170 |
. . . . . 6
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → (𝑤 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑦}) ⊆ 𝐴)) |
20 | | prodeq1 11516 |
. . . . . . 7
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶) |
21 | | iuneq1 3886 |
. . . . . . . 8
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) |
22 | 21 | prodeq1d 11527 |
. . . . . . 7
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷) |
23 | 20, 22 | eqeq12d 2185 |
. . . . . 6
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)) |
24 | 19, 23 | imbi12d 233 |
. . . . 5
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
25 | 24 | imbi2d 229 |
. . . 4
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)))) |
26 | | sseq1 3170 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
27 | | prodeq1 11516 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶) |
28 | | iuneq1 3886 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
29 | 28 | prodeq1d 11527 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷) |
30 | 27, 29 | eqeq12d 2185 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷)) |
31 | 26, 30 | imbi12d 233 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷))) |
32 | 31 | imbi2d 229 |
. . . 4
⊢ (𝑤 = 𝐴 → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷)))) |
33 | | prod0 11548 |
. . . . . 6
⊢
∏𝑗 ∈
∅ ∏𝑘 ∈
𝐵 𝐶 = 1 |
34 | | prod0 11548 |
. . . . . 6
⊢
∏𝑧 ∈
∅ 𝐷 =
1 |
35 | 33, 34 | eqtr4i 2194 |
. . . . 5
⊢
∏𝑗 ∈
∅ ∏𝑘 ∈
𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷 |
36 | 35 | 2a1i 27 |
. . . 4
⊢ (𝜑 → (∅ ⊆ 𝐴 → ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷)) |
37 | | ssun1 3290 |
. . . . . . . . 9
⊢ 𝑥 ⊆ (𝑥 ∪ {𝑦}) |
38 | | sstr 3155 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ (𝑥 ∪ {𝑦}) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑥 ⊆ 𝐴) |
39 | 37, 38 | mpan 422 |
. . . . . . . 8
⊢ ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → 𝑥 ⊆ 𝐴) |
40 | 39 | imim1i 60 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)) |
41 | | fprod2d.1 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) |
42 | 2 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝐴 ∈ Fin) |
43 | | fprod2d.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) |
44 | 43 | ad4ant14 511 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) |
45 | | fprod2d.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) |
46 | 45 | ad4ant14 511 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) |
47 | | simplrr 531 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ¬ 𝑦 ∈ 𝑥) |
48 | | simpr 109 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (𝑥 ∪ {𝑦}) ⊆ 𝐴) |
49 | | simplrl 530 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑥 ∈ Fin) |
50 | | biid 170 |
. . . . . . . . . 10
⊢
(∏𝑗 ∈
𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) |
51 | 41, 42, 44, 46, 47, 48, 49, 50 | fprod2dlemstep 11585 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷) |
52 | 51 | exp31 362 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
53 | 52 | a2d 26 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) → (((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
54 | 40, 53 | syl5 32 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥)) → ((𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
55 | 54 | expcom 115 |
. . . . 5
⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥) → (𝜑 → ((𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)))) |
56 | 55 | a2d 26 |
. . . 4
⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥) → ((𝜑 → (𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)) → (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)))) |
57 | 11, 18, 25, 32, 36, 56 | findcard2s 6868 |
. . 3
⊢ (𝐴 ∈ Fin → (𝜑 → (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷))) |
58 | 2, 57 | mpcom 36 |
. 2
⊢ (𝜑 → (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷)) |
59 | 1, 58 | mpi 15 |
1
⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷) |