Step |
Hyp |
Ref |
Expression |
0 |
|
cdsmm |
⊢ ⊕m |
1 |
|
vs |
⊢ 𝑠 |
2 |
|
cvv |
⊢ V |
3 |
|
vr |
⊢ 𝑟 |
4 |
1
|
cv |
⊢ 𝑠 |
5 |
|
cprds |
⊢ Xs |
6 |
3
|
cv |
⊢ 𝑟 |
7 |
4 6 5
|
co |
⊢ ( 𝑠 Xs 𝑟 ) |
8 |
|
cress |
⊢ ↾s |
9 |
|
vf |
⊢ 𝑓 |
10 |
|
vx |
⊢ 𝑥 |
11 |
6
|
cdm |
⊢ dom 𝑟 |
12 |
|
cbs |
⊢ Base |
13 |
10
|
cv |
⊢ 𝑥 |
14 |
13 6
|
cfv |
⊢ ( 𝑟 ‘ 𝑥 ) |
15 |
14 12
|
cfv |
⊢ ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) |
16 |
10 11 15
|
cixp |
⊢ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) |
17 |
9
|
cv |
⊢ 𝑓 |
18 |
13 17
|
cfv |
⊢ ( 𝑓 ‘ 𝑥 ) |
19 |
|
c0g |
⊢ 0g |
20 |
14 19
|
cfv |
⊢ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) |
21 |
18 20
|
wne |
⊢ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) |
22 |
21 10 11
|
crab |
⊢ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } |
23 |
|
cfn |
⊢ Fin |
24 |
22 23
|
wcel |
⊢ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin |
25 |
24 9 16
|
crab |
⊢ { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } |
26 |
7 25 8
|
co |
⊢ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) |
27 |
1 3 2 2 26
|
cmpo |
⊢ ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) ) |
28 |
0 27
|
wceq |
⊢ ⊕m = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) ) |