Detailed syntax breakdown of Definition df-prod
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class 𝐴 |
2 | | cB |
. . 3
class 𝐵 |
3 | | vk |
. . 3
setvar 𝑘 |
4 | 1, 2, 3 | cprod 15625 |
. 2
class
∏𝑘 ∈
𝐴 𝐵 |
5 | | vm |
. . . . . . . . 9
setvar 𝑚 |
6 | 5 | cv 1538 |
. . . . . . . 8
class 𝑚 |
7 | | cuz 12592 |
. . . . . . . 8
class
ℤ≥ |
8 | 6, 7 | cfv 6426 |
. . . . . . 7
class
(ℤ≥‘𝑚) |
9 | 1, 8 | wss 3886 |
. . . . . 6
wff 𝐴 ⊆
(ℤ≥‘𝑚) |
10 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
11 | 10 | cv 1538 |
. . . . . . . . . 10
class 𝑦 |
12 | | cc0 10881 |
. . . . . . . . . 10
class
0 |
13 | 11, 12 | wne 2943 |
. . . . . . . . 9
wff 𝑦 ≠ 0 |
14 | | cmul 10886 |
. . . . . . . . . . 11
class
· |
15 | | cz 12329 |
. . . . . . . . . . . 12
class
ℤ |
16 | 3 | cv 1538 |
. . . . . . . . . . . . . 14
class 𝑘 |
17 | 16, 1 | wcel 2106 |
. . . . . . . . . . . . 13
wff 𝑘 ∈ 𝐴 |
18 | | c1 10882 |
. . . . . . . . . . . . 13
class
1 |
19 | 17, 2, 18 | cif 4459 |
. . . . . . . . . . . 12
class if(𝑘 ∈ 𝐴, 𝐵, 1) |
20 | 3, 15, 19 | cmpt 5156 |
. . . . . . . . . . 11
class (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) |
21 | | vn |
. . . . . . . . . . . 12
setvar 𝑛 |
22 | 21 | cv 1538 |
. . . . . . . . . . 11
class 𝑛 |
23 | 14, 20, 22 | cseq 13731 |
. . . . . . . . . 10
class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) |
24 | | cli 15203 |
. . . . . . . . . 10
class
⇝ |
25 | 23, 11, 24 | wbr 5073 |
. . . . . . . . 9
wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 |
26 | 13, 25 | wa 396 |
. . . . . . . 8
wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) |
27 | 26, 10 | wex 1782 |
. . . . . . 7
wff
∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) |
28 | 27, 21, 8 | wrex 3065 |
. . . . . 6
wff
∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) |
29 | 14, 20, 6 | cseq 13731 |
. . . . . . 7
class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) |
30 | | vx |
. . . . . . . 8
setvar 𝑥 |
31 | 30 | cv 1538 |
. . . . . . 7
class 𝑥 |
32 | 29, 31, 24 | wbr 5073 |
. . . . . 6
wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 |
33 | 9, 28, 32 | w3a 1086 |
. . . . 5
wff (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) |
34 | 33, 5, 15 | wrex 3065 |
. . . 4
wff
∃𝑚 ∈
ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) |
35 | | cfz 13249 |
. . . . . . . . 9
class
... |
36 | 18, 6, 35 | co 7267 |
. . . . . . . 8
class
(1...𝑚) |
37 | | vf |
. . . . . . . . 9
setvar 𝑓 |
38 | 37 | cv 1538 |
. . . . . . . 8
class 𝑓 |
39 | 36, 1, 38 | wf1o 6425 |
. . . . . . 7
wff 𝑓:(1...𝑚)–1-1-onto→𝐴 |
40 | | cn 11983 |
. . . . . . . . . . 11
class
ℕ |
41 | 22, 38 | cfv 6426 |
. . . . . . . . . . . 12
class (𝑓‘𝑛) |
42 | 3, 41, 2 | csb 3831 |
. . . . . . . . . . 11
class
⦋(𝑓‘𝑛) / 𝑘⦌𝐵 |
43 | 21, 40, 42 | cmpt 5156 |
. . . . . . . . . 10
class (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
44 | 14, 43, 18 | cseq 13731 |
. . . . . . . . 9
class seq1(
· , (𝑛 ∈
ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) |
45 | 6, 44 | cfv 6426 |
. . . . . . . 8
class (seq1(
· , (𝑛 ∈
ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) |
46 | 31, 45 | wceq 1539 |
. . . . . . 7
wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) |
47 | 39, 46 | wa 396 |
. . . . . 6
wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
48 | 47, 37 | wex 1782 |
. . . . 5
wff
∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
49 | 48, 5, 40 | wrex 3065 |
. . . 4
wff
∃𝑚 ∈
ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) |
50 | 34, 49 | wo 844 |
. . 3
wff
(∃𝑚 ∈
ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) |
51 | 50, 30 | cio 6382 |
. 2
class
(℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
52 | 4, 51 | wceq 1539 |
1
wff
∏𝑘 ∈
𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |