Detailed syntax breakdown of Definition df-caragen
Step | Hyp | Ref
| Expression |
1 | | ccaragen 44011 |
. 2
class
CaraGen |
2 | | vo |
. . 3
setvar 𝑜 |
3 | | come 44009 |
. . 3
class
OutMeas |
4 | | va |
. . . . . . . . . 10
setvar 𝑎 |
5 | 4 | cv 1541 |
. . . . . . . . 9
class 𝑎 |
6 | | ve |
. . . . . . . . . 10
setvar 𝑒 |
7 | 6 | cv 1541 |
. . . . . . . . 9
class 𝑒 |
8 | 5, 7 | cin 3891 |
. . . . . . . 8
class (𝑎 ∩ 𝑒) |
9 | 2 | cv 1541 |
. . . . . . . 8
class 𝑜 |
10 | 8, 9 | cfv 6432 |
. . . . . . 7
class (𝑜‘(𝑎 ∩ 𝑒)) |
11 | 5, 7 | cdif 3889 |
. . . . . . . 8
class (𝑎 ∖ 𝑒) |
12 | 11, 9 | cfv 6432 |
. . . . . . 7
class (𝑜‘(𝑎 ∖ 𝑒)) |
13 | | cxad 12857 |
. . . . . . 7
class
+𝑒 |
14 | 10, 12, 13 | co 7272 |
. . . . . 6
class ((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) |
15 | 5, 9 | cfv 6432 |
. . . . . 6
class (𝑜‘𝑎) |
16 | 14, 15 | wceq 1542 |
. . . . 5
wff ((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎) |
17 | 9 | cdm 5590 |
. . . . . . 7
class dom 𝑜 |
18 | 17 | cuni 4845 |
. . . . . 6
class ∪ dom 𝑜 |
19 | 18 | cpw 4539 |
. . . . 5
class 𝒫
∪ dom 𝑜 |
20 | 16, 4, 19 | wral 3066 |
. . . 4
wff
∀𝑎 ∈
𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎) |
21 | 20, 6, 19 | crab 3070 |
. . 3
class {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)} |
22 | 2, 3, 21 | cmpt 5162 |
. 2
class (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)}) |
23 | 1, 22 | wceq 1542 |
1
wff CaraGen =
(𝑜 ∈ OutMeas ↦
{𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)}) |