Step |
Hyp |
Ref |
Expression |
0 |
|
ccnf |
⊢ CNF |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
con0 |
⊢ On |
3 |
|
vy |
⊢ 𝑦 |
4 |
|
vf |
⊢ 𝑓 |
5 |
|
vg |
⊢ 𝑔 |
6 |
1
|
cv |
⊢ 𝑥 |
7 |
|
cmap |
⊢ ↑m |
8 |
3
|
cv |
⊢ 𝑦 |
9 |
6 8 7
|
co |
⊢ ( 𝑥 ↑m 𝑦 ) |
10 |
5
|
cv |
⊢ 𝑔 |
11 |
|
cfsupp |
⊢ finSupp |
12 |
|
c0 |
⊢ ∅ |
13 |
10 12 11
|
wbr |
⊢ 𝑔 finSupp ∅ |
14 |
13 5 9
|
crab |
⊢ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } |
15 |
|
cep |
⊢ E |
16 |
4
|
cv |
⊢ 𝑓 |
17 |
|
csupp |
⊢ supp |
18 |
16 12 17
|
co |
⊢ ( 𝑓 supp ∅ ) |
19 |
18 15
|
coi |
⊢ OrdIso ( E , ( 𝑓 supp ∅ ) ) |
20 |
|
vh |
⊢ ℎ |
21 |
|
vk |
⊢ 𝑘 |
22 |
|
cvv |
⊢ V |
23 |
|
vz |
⊢ 𝑧 |
24 |
|
coe |
⊢ ↑o |
25 |
20
|
cv |
⊢ ℎ |
26 |
21
|
cv |
⊢ 𝑘 |
27 |
26 25
|
cfv |
⊢ ( ℎ ‘ 𝑘 ) |
28 |
6 27 24
|
co |
⊢ ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) |
29 |
|
comu |
⊢ ·o |
30 |
27 16
|
cfv |
⊢ ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) |
31 |
28 30 29
|
co |
⊢ ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) |
32 |
|
coa |
⊢ +o |
33 |
23
|
cv |
⊢ 𝑧 |
34 |
31 33 32
|
co |
⊢ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) |
35 |
21 23 22 22 34
|
cmpo |
⊢ ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) |
36 |
35 12
|
cseqom |
⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) |
37 |
25
|
cdm |
⊢ dom ℎ |
38 |
37 36
|
cfv |
⊢ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) |
39 |
20 19 38
|
csb |
⊢ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) |
40 |
4 14 39
|
cmpt |
⊢ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) |
41 |
1 3 2 2 40
|
cmpo |
⊢ ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) ) |
42 |
0 41
|
wceq |
⊢ CNF = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥 ↑m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) ) |