Step | Hyp | Ref
| Expression |
1 | | fprodcl2lem.5 |
. . 3
⊢ (𝜑 → 𝐴 ≠ ∅) |
2 | 1 | neneqd 2348 |
. 2
⊢ (𝜑 → ¬ 𝐴 = ∅) |
3 | | eqeq1 2164 |
. . . . 5
⊢ (𝑤 = ∅ → (𝑤 = ∅ ↔ ∅ =
∅)) |
4 | | prodeq1 11454 |
. . . . . 6
⊢ (𝑤 = ∅ → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
5 | 4 | eleq1d 2226 |
. . . . 5
⊢ (𝑤 = ∅ → (∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆 ↔ ∏𝑘 ∈ ∅ 𝐵 ∈ 𝑆)) |
6 | 3, 5 | orbi12d 783 |
. . . 4
⊢ (𝑤 = ∅ → ((𝑤 = ∅ ∨ ∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆) ↔ (∅ = ∅ ∨
∏𝑘 ∈ ∅
𝐵 ∈ 𝑆))) |
7 | | eqeq1 2164 |
. . . . 5
⊢ (𝑤 = 𝑦 → (𝑤 = ∅ ↔ 𝑦 = ∅)) |
8 | | prodeq1 11454 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ 𝑦 𝐵) |
9 | 8 | eleq1d 2226 |
. . . . 5
⊢ (𝑤 = 𝑦 → (∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆 ↔ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆)) |
10 | 7, 9 | orbi12d 783 |
. . . 4
⊢ (𝑤 = 𝑦 → ((𝑤 = ∅ ∨ ∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆) ↔ (𝑦 = ∅ ∨ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆))) |
11 | | eqeq1 2164 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤 = ∅ ↔ (𝑦 ∪ {𝑧}) = ∅)) |
12 | | prodeq1 11454 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) |
13 | 12 | eleq1d 2226 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆 ↔ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆)) |
14 | 11, 13 | orbi12d 783 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤 = ∅ ∨ ∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆) ↔ ((𝑦 ∪ {𝑧}) = ∅ ∨ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆))) |
15 | | eqeq1 2164 |
. . . . 5
⊢ (𝑤 = 𝐴 → (𝑤 = ∅ ↔ 𝐴 = ∅)) |
16 | | prodeq1 11454 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ∏𝑘 ∈ 𝑤 𝐵 = ∏𝑘 ∈ 𝐴 𝐵) |
17 | 16 | eleq1d 2226 |
. . . . 5
⊢ (𝑤 = 𝐴 → (∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆 ↔ ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)) |
18 | 15, 17 | orbi12d 783 |
. . . 4
⊢ (𝑤 = 𝐴 → ((𝑤 = ∅ ∨ ∏𝑘 ∈ 𝑤 𝐵 ∈ 𝑆) ↔ (𝐴 = ∅ ∨ ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆))) |
19 | | eqidd 2158 |
. . . . 5
⊢ (𝜑 → ∅ =
∅) |
20 | 19 | orcd 723 |
. . . 4
⊢ (𝜑 → (∅ = ∅ ∨
∏𝑘 ∈ ∅
𝐵 ∈ 𝑆)) |
21 | | nfcsb1v 3064 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵 |
22 | | simplr 520 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
23 | | simprr 522 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
24 | 23 | eldifbd 3114 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
25 | | fprodcllem.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
26 | 25 | ad3antrrr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑆 ⊆ ℂ) |
27 | | simplll 523 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
28 | | simplrl 525 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑦 ⊆ 𝐴) |
29 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦) |
30 | 28, 29 | sseldd 3129 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴) |
31 | | fprodcllem.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) |
32 | 27, 30, 31 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ 𝑆) |
33 | 26, 32 | sseldd 3129 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ) |
34 | 25 | ad2antrr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑆 ⊆ ℂ) |
35 | | simpll 519 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝜑) |
36 | 23 | eldifad 3113 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴) |
37 | 31 | ralrimiva 2530 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |
38 | | nfv 1508 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧 𝐵 ∈ 𝑆 |
39 | 21 | nfel1 2310 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆 |
40 | | csbeq1a 3040 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑘⦌𝐵) |
41 | 40 | eleq1d 2226 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝐵 ∈ 𝑆 ↔ ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆)) |
42 | 38, 39, 41 | cbvral 2676 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ 𝑆 ↔ ∀𝑧 ∈ 𝐴 ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆) |
43 | 37, 42 | sylib 121 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆) |
44 | 43 | r19.21bi 2545 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆) |
45 | 35, 36, 44 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆) |
46 | 34, 45 | sseldd 3129 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) |
47 | 21, 22, 23, 24, 33, 46, 40 | fprodunsn 11505 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵)) |
48 | 47 | adantr 274 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵)) |
49 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → 𝑦 = ∅) |
50 | 49 | prodeq1d 11465 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → ∏𝑘 ∈ 𝑦 𝐵 = ∏𝑘 ∈ ∅ 𝐵) |
51 | | prod0 11486 |
. . . . . . . . . . . 12
⊢
∏𝑘 ∈
∅ 𝐵 =
1 |
52 | 50, 51 | eqtrdi 2206 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → ∏𝑘 ∈ 𝑦 𝐵 = 1) |
53 | 52 | oveq1d 5840 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) = (1 · ⦋𝑧 / 𝑘⦌𝐵)) |
54 | 46 | adantr 274 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) |
55 | 54 | mulid2d 7897 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → (1 ·
⦋𝑧 / 𝑘⦌𝐵) = ⦋𝑧 / 𝑘⦌𝐵) |
56 | 53, 55 | eqtrd 2190 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) = ⦋𝑧 / 𝑘⦌𝐵) |
57 | 45 | adantr 274 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆) |
58 | 56, 57 | eqeltrd 2234 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) ∈ 𝑆) |
59 | 48, 58 | eqeltrd 2234 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆) |
60 | 59 | olcd 724 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑦 = ∅) → ((𝑦 ∪ {𝑧}) = ∅ ∨ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆)) |
61 | 60 | ex 114 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑦 = ∅ → ((𝑦 ∪ {𝑧}) = ∅ ∨ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆))) |
62 | 47 | adantr 274 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵)) |
63 | | fprodcllem.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
64 | 63 | ralrimivva 2539 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 · 𝑦) ∈ 𝑆) |
65 | | oveq1 5832 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑢 → (𝑥 · 𝑦) = (𝑢 · 𝑦)) |
66 | 65 | eleq1d 2226 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → ((𝑥 · 𝑦) ∈ 𝑆 ↔ (𝑢 · 𝑦) ∈ 𝑆)) |
67 | | oveq2 5833 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (𝑢 · 𝑦) = (𝑢 · 𝑣)) |
68 | 67 | eleq1d 2226 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑣 → ((𝑢 · 𝑦) ∈ 𝑆 ↔ (𝑢 · 𝑣) ∈ 𝑆)) |
69 | 66, 68 | cbvral2v 2691 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 (𝑥 · 𝑦) ∈ 𝑆 ↔ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (𝑢 · 𝑣) ∈ 𝑆) |
70 | 64, 69 | sylib 121 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (𝑢 · 𝑣) ∈ 𝑆) |
71 | 70 | ad3antrrr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (𝑢 · 𝑣) ∈ 𝑆) |
72 | | simpr 109 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) |
73 | 45 | adantr 274 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆) |
74 | | oveq1 5832 |
. . . . . . . . . . . 12
⊢ (𝑢 = ∏𝑘 ∈ 𝑦 𝐵 → (𝑢 · 𝑣) = (∏𝑘 ∈ 𝑦 𝐵 · 𝑣)) |
75 | 74 | eleq1d 2226 |
. . . . . . . . . . 11
⊢ (𝑢 = ∏𝑘 ∈ 𝑦 𝐵 → ((𝑢 · 𝑣) ∈ 𝑆 ↔ (∏𝑘 ∈ 𝑦 𝐵 · 𝑣) ∈ 𝑆)) |
76 | | oveq2 5833 |
. . . . . . . . . . . 12
⊢ (𝑣 = ⦋𝑧 / 𝑘⦌𝐵 → (∏𝑘 ∈ 𝑦 𝐵 · 𝑣) = (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵)) |
77 | 76 | eleq1d 2226 |
. . . . . . . . . . 11
⊢ (𝑣 = ⦋𝑧 / 𝑘⦌𝐵 → ((∏𝑘 ∈ 𝑦 𝐵 · 𝑣) ∈ 𝑆 ↔ (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) ∈ 𝑆)) |
78 | 75, 77 | rspc2v 2829 |
. . . . . . . . . 10
⊢
((∏𝑘 ∈
𝑦 𝐵 ∈ 𝑆 ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ 𝑆) → (∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (𝑢 · 𝑣) ∈ 𝑆 → (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) ∈ 𝑆)) |
79 | 72, 73, 78 | syl2anc 409 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → (∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 (𝑢 · 𝑣) ∈ 𝑆 → (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) ∈ 𝑆)) |
80 | 71, 79 | mpd 13 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → (∏𝑘 ∈ 𝑦 𝐵 · ⦋𝑧 / 𝑘⦌𝐵) ∈ 𝑆) |
81 | 62, 80 | eqeltrd 2234 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆) |
82 | 81 | olcd 724 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → ((𝑦 ∪ {𝑧}) = ∅ ∨ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆)) |
83 | 82 | ex 114 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆 → ((𝑦 ∪ {𝑧}) = ∅ ∨ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆))) |
84 | 61, 83 | jaod 707 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝑦 = ∅ ∨ ∏𝑘 ∈ 𝑦 𝐵 ∈ 𝑆) → ((𝑦 ∪ {𝑧}) = ∅ ∨ ∏𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ 𝑆))) |
85 | | fprodcllem.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
86 | 6, 10, 14, 18, 20, 84, 85 | findcard2sd 6838 |
. . 3
⊢ (𝜑 → (𝐴 = ∅ ∨ ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)) |
87 | 86 | orcomd 719 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∨ 𝐴 = ∅)) |
88 | 2, 87 | ecased 1331 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) |