| Step | Hyp | Ref
| Expression |
| 1 | | ssid 4006 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
| 2 | | fprod2d.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 3 | | sseq1 4009 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
| 4 | | prodeq1 15943 |
. . . . . . 7
⊢ (𝑤 = ∅ → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶) |
| 5 | | iuneq1 5008 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → ∪ 𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ ∅ ({𝑗} × 𝐵)) |
| 6 | | 0iun 5063 |
. . . . . . . . 9
⊢ ∪ 𝑗 ∈ ∅ ({𝑗} × 𝐵) = ∅ |
| 7 | 5, 6 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑤 = ∅ → ∪ 𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∅) |
| 8 | 7 | prodeq1d 15956 |
. . . . . . 7
⊢ (𝑤 = ∅ → ∏𝑧 ∈ ∪ 𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∅ 𝐷) |
| 9 | 4, 8 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑤 = ∅ → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷)) |
| 10 | 3, 9 | imbi12d 344 |
. . . . 5
⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ (∅ ⊆ 𝐴 → ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷))) |
| 11 | 10 | imbi2d 340 |
. . . 4
⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → (∅ ⊆ 𝐴 → ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷)))) |
| 12 | | sseq1 4009 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝑤 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴)) |
| 13 | | prodeq1 15943 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶) |
| 14 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)) |
| 15 | 14 | prodeq1d 15956 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) |
| 16 | 13, 15 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)) |
| 17 | 12, 16 | imbi12d 344 |
. . . . 5
⊢ (𝑤 = 𝑥 → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ (𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷))) |
| 18 | 17 | imbi2d 340 |
. . . 4
⊢ (𝑤 = 𝑥 → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → (𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)))) |
| 19 | | sseq1 4009 |
. . . . . 6
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → (𝑤 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑦}) ⊆ 𝐴)) |
| 20 | | prodeq1 15943 |
. . . . . . 7
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶) |
| 21 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) |
| 22 | 21 | prodeq1d 15956 |
. . . . . . 7
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷) |
| 23 | 20, 22 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)) |
| 24 | 19, 23 | imbi12d 344 |
. . . . 5
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
| 25 | 24 | imbi2d 340 |
. . . 4
⊢ (𝑤 = (𝑥 ∪ {𝑦}) → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)))) |
| 26 | | sseq1 4009 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (𝑤 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
| 27 | | prodeq1 15943 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶) |
| 28 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵) = ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 29 | 28 | prodeq1d 15956 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷) |
| 30 | 27, 29 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷)) |
| 31 | 26, 30 | imbi12d 344 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷) ↔ (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷))) |
| 32 | 31 | imbi2d 340 |
. . . 4
⊢ (𝑤 = 𝐴 → ((𝜑 → (𝑤 ⊆ 𝐴 → ∏𝑗 ∈ 𝑤 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑤 ({𝑗} × 𝐵)𝐷)) ↔ (𝜑 → (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷)))) |
| 33 | | prod0 15979 |
. . . . . 6
⊢
∏𝑗 ∈
∅ ∏𝑘 ∈
𝐵 𝐶 = 1 |
| 34 | | prod0 15979 |
. . . . . 6
⊢
∏𝑧 ∈
∅ 𝐷 =
1 |
| 35 | 33, 34 | eqtr4i 2768 |
. . . . 5
⊢
∏𝑗 ∈
∅ ∏𝑘 ∈
𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷 |
| 36 | 35 | 2a1i 12 |
. . . 4
⊢ (𝜑 → (∅ ⊆ 𝐴 → ∏𝑗 ∈ ∅ ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∅ 𝐷)) |
| 37 | | ssun1 4178 |
. . . . . . . . . 10
⊢ 𝑥 ⊆ (𝑥 ∪ {𝑦}) |
| 38 | | sstr 3992 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ (𝑥 ∪ {𝑦}) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑥 ⊆ 𝐴) |
| 39 | 37, 38 | mpan 690 |
. . . . . . . . 9
⊢ ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → 𝑥 ⊆ 𝐴) |
| 40 | 39 | imim1i 63 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)) |
| 41 | | fprod2d.1 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) |
| 42 | 2 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝐴 ∈ Fin) |
| 43 | | fprod2d.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) |
| 44 | 43 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ Fin) |
| 45 | | fprod2d.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) |
| 46 | 45 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) |
| 47 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ¬ 𝑦 ∈ 𝑥) |
| 48 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (𝑥 ∪ {𝑦}) ⊆ 𝐴) |
| 49 | | biid 261 |
. . . . . . . . . . 11
⊢
(∏𝑗 ∈
𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 ↔ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) |
| 50 | 41, 42, 44, 46, 47, 48, 49 | fprod2dlem 16016 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷) |
| 51 | 50 | exp31 419 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
| 52 | 51 | a2d 29 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) → (((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
| 53 | 40, 52 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑦 ∈ 𝑥) → ((𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷))) |
| 54 | 53 | expcom 413 |
. . . . . 6
⊢ (¬
𝑦 ∈ 𝑥 → (𝜑 → ((𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)))) |
| 55 | 54 | a2d 29 |
. . . . 5
⊢ (¬
𝑦 ∈ 𝑥 → ((𝜑 → (𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)) → (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)))) |
| 56 | 55 | adantl 481 |
. . . 4
⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑦 ∈ 𝑥) → ((𝜑 → (𝑥 ⊆ 𝐴 → ∏𝑗 ∈ 𝑥 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝑥 ({𝑗} × 𝐵)𝐷)) → (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ∏𝑗 ∈ (𝑥 ∪ {𝑦})∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)))) |
| 57 | 11, 18, 25, 32, 36, 56 | findcard2s 9205 |
. . 3
⊢ (𝐴 ∈ Fin → (𝜑 → (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷))) |
| 58 | 2, 57 | mpcom 38 |
. 2
⊢ (𝜑 → (𝐴 ⊆ 𝐴 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷)) |
| 59 | 1, 58 | mpi 20 |
1
⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐷) |