Step | Hyp | Ref
| Expression |
1 | | df-proddc 11514 |
. 2
⊢
∏𝑘 ∈
𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈
(ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) |
2 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑘ℤ |
3 | | nfcprod1.1 |
. . . . . . . 8
⊢
Ⅎ𝑘𝐴 |
4 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑘(ℤ≥‘𝑚) |
5 | 3, 4 | nfss 3140 |
. . . . . . 7
⊢
Ⅎ𝑘 𝐴 ⊆
(ℤ≥‘𝑚) |
6 | 3 | nfcri 2306 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 |
7 | 6 | nfdc 1652 |
. . . . . . . 8
⊢
Ⅎ𝑘DECID 𝑗 ∈ 𝐴 |
8 | 4, 7 | nfralxy 2508 |
. . . . . . 7
⊢
Ⅎ𝑘∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 |
9 | 5, 8 | nfan 1558 |
. . . . . 6
⊢
Ⅎ𝑘(𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) |
10 | | nfv 1521 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑦 # 0 |
11 | | nfcv 2312 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑛 |
12 | | nfcv 2312 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘
· |
13 | | nfmpt1 4082 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) |
14 | 11, 12, 13 | nfseq 10411 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) |
15 | | nfcv 2312 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘
⇝ |
16 | | nfcv 2312 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑦 |
17 | 14, 15, 16 | nfbr 4035 |
. . . . . . . . . 10
⊢
Ⅎ𝑘seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 |
18 | 10, 17 | nfan 1558 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) |
19 | 18 | nfex 1630 |
. . . . . . . 8
⊢
Ⅎ𝑘∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) |
20 | 4, 19 | nfrexxy 2509 |
. . . . . . 7
⊢
Ⅎ𝑘∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) |
21 | | nfcv 2312 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝑚 |
22 | 21, 12, 13 | nfseq 10411 |
. . . . . . . 8
⊢
Ⅎ𝑘seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) |
23 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑥 |
24 | 22, 15, 23 | nfbr 4035 |
. . . . . . 7
⊢
Ⅎ𝑘seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 |
25 | 20, 24 | nfan 1558 |
. . . . . 6
⊢
Ⅎ𝑘(∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) |
26 | 9, 25 | nfan 1558 |
. . . . 5
⊢
Ⅎ𝑘((𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) |
27 | 2, 26 | nfrexxy 2509 |
. . . 4
⊢
Ⅎ𝑘∃𝑚 ∈ ℤ ((𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) |
28 | | nfcv 2312 |
. . . . 5
⊢
Ⅎ𝑘ℕ |
29 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑓 |
30 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑘(1...𝑚) |
31 | 29, 30, 3 | nff1o 5440 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑓:(1...𝑚)–1-1-onto→𝐴 |
32 | | nfcv 2312 |
. . . . . . . . . 10
⊢
Ⅎ𝑘1 |
33 | | nfv 1521 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘 𝑛 ≤ 𝑚 |
34 | | nfcsb1v 3082 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋(𝑓‘𝑛) / 𝑘⦌𝐵 |
35 | 33, 34, 32 | nfif 3554 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) |
36 | 28, 35 | nfmpt 4081 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) |
37 | 32, 12, 36 | nfseq 10411 |
. . . . . . . . 9
⊢
Ⅎ𝑘seq1(
· , (𝑛 ∈
ℕ ↦ if(𝑛 ≤
𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) |
38 | 37, 21 | nffv 5506 |
. . . . . . . 8
⊢
Ⅎ𝑘(seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) |
39 | 38 | nfeq2 2324 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) |
40 | 31, 39 | nfan 1558 |
. . . . . 6
⊢
Ⅎ𝑘(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) |
41 | 40 | nfex 1630 |
. . . . 5
⊢
Ⅎ𝑘∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) |
42 | 28, 41 | nfrexxy 2509 |
. . . 4
⊢
Ⅎ𝑘∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) |
43 | 27, 42 | nfor 1567 |
. . 3
⊢
Ⅎ𝑘(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈
(ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) |
44 | 43 | nfiotaw 5164 |
. 2
⊢
Ⅎ𝑘(℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈
(ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) |
45 | 1, 44 | nfcxfr 2309 |
1
⊢
Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵 |