Step |
Hyp |
Ref |
Expression |
0 |
|
ccaragen |
⊢ CaraGen |
1 |
|
vo |
⊢ 𝑜 |
2 |
|
come |
⊢ OutMeas |
3 |
|
ve |
⊢ 𝑒 |
4 |
1
|
cv |
⊢ 𝑜 |
5 |
4
|
cdm |
⊢ dom 𝑜 |
6 |
5
|
cuni |
⊢ ∪ dom 𝑜 |
7 |
6
|
cpw |
⊢ 𝒫 ∪ dom 𝑜 |
8 |
|
va |
⊢ 𝑎 |
9 |
8
|
cv |
⊢ 𝑎 |
10 |
3
|
cv |
⊢ 𝑒 |
11 |
9 10
|
cin |
⊢ ( 𝑎 ∩ 𝑒 ) |
12 |
11 4
|
cfv |
⊢ ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) |
13 |
|
cxad |
⊢ +𝑒 |
14 |
9 10
|
cdif |
⊢ ( 𝑎 ∖ 𝑒 ) |
15 |
14 4
|
cfv |
⊢ ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) |
16 |
12 15 13
|
co |
⊢ ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) |
17 |
9 4
|
cfv |
⊢ ( 𝑜 ‘ 𝑎 ) |
18 |
16 17
|
wceq |
⊢ ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) |
19 |
18 8 7
|
wral |
⊢ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) |
20 |
19 3 7
|
crab |
⊢ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } |
21 |
1 2 20
|
cmpt |
⊢ ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } ) |
22 |
0 21
|
wceq |
⊢ CaraGen = ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } ) |