Detailed syntax breakdown of Definition df-cnf
Step | Hyp | Ref
| Expression |
1 | | ccnf 8558 |
. 2
class
CNF |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | con0 5723 |
. . 3
class
On |
5 | | vf |
. . . 4
setvar 𝑓 |
6 | | vg |
. . . . . . 7
setvar 𝑔 |
7 | 6 | cv 1482 |
. . . . . 6
class 𝑔 |
8 | | c0 3915 |
. . . . . 6
class
∅ |
9 | | cfsupp 8275 |
. . . . . 6
class
finSupp |
10 | 7, 8, 9 | wbr 4653 |
. . . . 5
wff 𝑔 finSupp
∅ |
11 | 2 | cv 1482 |
. . . . . 6
class 𝑥 |
12 | 3 | cv 1482 |
. . . . . 6
class 𝑦 |
13 | | cmap 7857 |
. . . . . 6
class
↑𝑚 |
14 | 11, 12, 13 | co 6650 |
. . . . 5
class (𝑥 ↑𝑚
𝑦) |
15 | 10, 6, 14 | crab 2916 |
. . . 4
class {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} |
16 | | vh |
. . . . 5
setvar ℎ |
17 | 5 | cv 1482 |
. . . . . . 7
class 𝑓 |
18 | | csupp 7295 |
. . . . . . 7
class
supp |
19 | 17, 8, 18 | co 6650 |
. . . . . 6
class (𝑓 supp ∅) |
20 | | cep 5028 |
. . . . . 6
class
E |
21 | 19, 20 | coi 8414 |
. . . . 5
class OrdIso( E
, (𝑓 supp
∅)) |
22 | 16 | cv 1482 |
. . . . . . 7
class ℎ |
23 | 22 | cdm 5114 |
. . . . . 6
class dom ℎ |
24 | | vk |
. . . . . . . 8
setvar 𝑘 |
25 | | vz |
. . . . . . . 8
setvar 𝑧 |
26 | | cvv 3200 |
. . . . . . . 8
class
V |
27 | 24 | cv 1482 |
. . . . . . . . . . . 12
class 𝑘 |
28 | 27, 22 | cfv 5888 |
. . . . . . . . . . 11
class (ℎ‘𝑘) |
29 | | coe 7559 |
. . . . . . . . . . 11
class
↑𝑜 |
30 | 11, 28, 29 | co 6650 |
. . . . . . . . . 10
class (𝑥 ↑𝑜
(ℎ‘𝑘)) |
31 | 28, 17 | cfv 5888 |
. . . . . . . . . 10
class (𝑓‘(ℎ‘𝑘)) |
32 | | comu 7558 |
. . . . . . . . . 10
class
·𝑜 |
33 | 30, 31, 32 | co 6650 |
. . . . . . . . 9
class ((𝑥 ↑𝑜
(ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) |
34 | 25 | cv 1482 |
. . . . . . . . 9
class 𝑧 |
35 | | coa 7557 |
. . . . . . . . 9
class
+𝑜 |
36 | 33, 34, 35 | co 6650 |
. . . . . . . 8
class (((𝑥 ↑𝑜
(ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧) |
37 | 24, 25, 26, 26, 36 | cmpt2 6652 |
. . . . . . 7
class (𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)) |
38 | 37, 8 | cseqom 7542 |
. . . . . 6
class
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅) |
39 | 23, 38 | cfv 5888 |
. . . . 5
class
(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ) |
40 | 16, 21, 39 | csb 3533 |
. . . 4
class
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ) |
41 | 5, 15, 40 | cmpt 4729 |
. . 3
class (𝑓 ∈ {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ)) |
42 | 2, 3, 4, 4, 41 | cmpt2 6652 |
. 2
class (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))) |
43 | 1, 42 | wceq 1483 |
1
wff CNF =
(𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))) |