| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-prod 15940 | . 2
⊢
∏𝑘 ∈
𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) | 
| 2 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑘ℤ | 
| 3 |  | nfcprod1.1 | . . . . . . 7
⊢
Ⅎ𝑘𝐴 | 
| 4 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑘(ℤ≥‘𝑚) | 
| 5 | 3, 4 | nfss 3976 | . . . . . 6
⊢
Ⅎ𝑘 𝐴 ⊆
(ℤ≥‘𝑚) | 
| 6 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑘 𝑦 ≠ 0 | 
| 7 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑘𝑛 | 
| 8 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑘
· | 
| 9 |  | nfmpt1 5250 | . . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) | 
| 10 | 7, 8, 9 | nfseq 14052 | . . . . . . . . . 10
⊢
Ⅎ𝑘seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) | 
| 11 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑘
⇝ | 
| 12 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑘𝑦 | 
| 13 | 10, 11, 12 | nfbr 5190 | . . . . . . . . 9
⊢
Ⅎ𝑘seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 | 
| 14 | 6, 13 | nfan 1899 | . . . . . . . 8
⊢
Ⅎ𝑘(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) | 
| 15 | 14 | nfex 2324 | . . . . . . 7
⊢
Ⅎ𝑘∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) | 
| 16 | 4, 15 | nfrexw 3313 | . . . . . 6
⊢
Ⅎ𝑘∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) | 
| 17 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑘𝑚 | 
| 18 | 17, 8, 9 | nfseq 14052 | . . . . . . 7
⊢
Ⅎ𝑘seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) | 
| 19 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑘𝑥 | 
| 20 | 18, 11, 19 | nfbr 5190 | . . . . . 6
⊢
Ⅎ𝑘seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 | 
| 21 | 5, 16, 20 | nf3an 1901 | . . . . 5
⊢
Ⅎ𝑘(𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) | 
| 22 | 2, 21 | nfrexw 3313 | . . . 4
⊢
Ⅎ𝑘∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) | 
| 23 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑘ℕ | 
| 24 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑘𝑓 | 
| 25 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑘(1...𝑚) | 
| 26 | 24, 25, 3 | nff1o 6846 | . . . . . . 7
⊢
Ⅎ𝑘 𝑓:(1...𝑚)–1-1-onto→𝐴 | 
| 27 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑘1 | 
| 28 |  | nfcsb1v 3923 | . . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(𝑓‘𝑛) / 𝑘⦌𝐵 | 
| 29 | 23, 28 | nfmpt 5249 | . . . . . . . . . 10
⊢
Ⅎ𝑘(𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) | 
| 30 | 27, 8, 29 | nfseq 14052 | . . . . . . . . 9
⊢
Ⅎ𝑘seq1(
· , (𝑛 ∈
ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) | 
| 31 | 30, 17 | nffv 6916 | . . . . . . . 8
⊢
Ⅎ𝑘(seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) | 
| 32 | 31 | nfeq2 2923 | . . . . . . 7
⊢
Ⅎ𝑘 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) | 
| 33 | 26, 32 | nfan 1899 | . . . . . 6
⊢
Ⅎ𝑘(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) | 
| 34 | 33 | nfex 2324 | . . . . 5
⊢
Ⅎ𝑘∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) | 
| 35 | 23, 34 | nfrexw 3313 | . . . 4
⊢
Ⅎ𝑘∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) | 
| 36 | 22, 35 | nfor 1904 | . . 3
⊢
Ⅎ𝑘(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) | 
| 37 | 36 | nfiotaw 6518 | . 2
⊢
Ⅎ𝑘(℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) | 
| 38 | 1, 37 | nfcxfr 2903 | 1
⊢
Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵 |