| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-prod 15941 | . 2
⊢
∏𝑘 ∈
𝐴 𝐵 = (℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) | 
| 2 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑥ℤ | 
| 3 |  | nfcprod.1 | . . . . . . 7
⊢
Ⅎ𝑥𝐴 | 
| 4 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑥(ℤ≥‘𝑚) | 
| 5 | 3, 4 | nfss 3975 | . . . . . 6
⊢
Ⅎ𝑥 𝐴 ⊆
(ℤ≥‘𝑚) | 
| 6 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑥 𝑧 ≠ 0 | 
| 7 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑥𝑛 | 
| 8 |  | nfcv 2904 | . . . . . . . . . . 11
⊢
Ⅎ𝑥
· | 
| 9 | 3 | nfcri 2896 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑘 ∈ 𝐴 | 
| 10 |  | nfcprod.2 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐵 | 
| 11 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥1 | 
| 12 | 9, 10, 11 | nfif 4555 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥if(𝑘 ∈ 𝐴, 𝐵, 1) | 
| 13 | 2, 12 | nfmpt 5248 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) | 
| 14 | 7, 8, 13 | nfseq 14053 | . . . . . . . . . 10
⊢
Ⅎ𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) | 
| 15 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑥
⇝ | 
| 16 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝑧 | 
| 17 | 14, 15, 16 | nfbr 5189 | . . . . . . . . 9
⊢
Ⅎ𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧 | 
| 18 | 6, 17 | nfan 1898 | . . . . . . . 8
⊢
Ⅎ𝑥(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) | 
| 19 | 18 | nfex 2323 | . . . . . . 7
⊢
Ⅎ𝑥∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) | 
| 20 | 4, 19 | nfrexw 3312 | . . . . . 6
⊢
Ⅎ𝑥∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) | 
| 21 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥𝑚 | 
| 22 | 21, 8, 13 | nfseq 14053 | . . . . . . 7
⊢
Ⅎ𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) | 
| 23 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑥𝑦 | 
| 24 | 22, 15, 23 | nfbr 5189 | . . . . . 6
⊢
Ⅎ𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 | 
| 25 | 5, 20, 24 | nf3an 1900 | . . . . 5
⊢
Ⅎ𝑥(𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) | 
| 26 | 2, 25 | nfrexw 3312 | . . . 4
⊢
Ⅎ𝑥∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) | 
| 27 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑥ℕ | 
| 28 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥𝑓 | 
| 29 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥(1...𝑚) | 
| 30 | 28, 29, 3 | nff1o 6845 | . . . . . . 7
⊢
Ⅎ𝑥 𝑓:(1...𝑚)–1-1-onto→𝐴 | 
| 31 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑓‘𝑛) | 
| 32 | 31, 10 | nfcsbw 3924 | . . . . . . . . . . 11
⊢
Ⅎ𝑥⦋(𝑓‘𝑛) / 𝑘⦌𝐵 | 
| 33 | 27, 32 | nfmpt 5248 | . . . . . . . . . 10
⊢
Ⅎ𝑥(𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) | 
| 34 | 11, 8, 33 | nfseq 14053 | . . . . . . . . 9
⊢
Ⅎ𝑥seq1(
· , (𝑛 ∈
ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) | 
| 35 | 34, 21 | nffv 6915 | . . . . . . . 8
⊢
Ⅎ𝑥(seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) | 
| 36 | 35 | nfeq2 2922 | . . . . . . 7
⊢
Ⅎ𝑥 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) | 
| 37 | 30, 36 | nfan 1898 | . . . . . 6
⊢
Ⅎ𝑥(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) | 
| 38 | 37 | nfex 2323 | . . . . 5
⊢
Ⅎ𝑥∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) | 
| 39 | 27, 38 | nfrexw 3312 | . . . 4
⊢
Ⅎ𝑥∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) | 
| 40 | 26, 39 | nfor 1903 | . . 3
⊢
Ⅎ𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) | 
| 41 | 40 | nfiotaw 6517 | . 2
⊢
Ⅎ𝑥(℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) | 
| 42 | 1, 41 | nfcxfr 2902 | 1
⊢
Ⅎ𝑥∏𝑘 ∈ 𝐴 𝐵 |