Step | Hyp | Ref
| Expression |
1 | | cfae 33267 |
. 2
class ~
a.e. |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vm |
. . 3
setvar 𝑚 |
4 | | cvv 3475 |
. . 3
class
V |
5 | | cmeas 33224 |
. . . . 5
class
measures |
6 | 5 | crn 5678 |
. . . 4
class ran
measures |
7 | 6 | cuni 4909 |
. . 3
class ∪ ran measures |
8 | | vf |
. . . . . . . 8
setvar 𝑓 |
9 | 8 | cv 1541 |
. . . . . . 7
class 𝑓 |
10 | 2 | cv 1541 |
. . . . . . . . 9
class 𝑟 |
11 | 10 | cdm 5677 |
. . . . . . . 8
class dom 𝑟 |
12 | 3 | cv 1541 |
. . . . . . . . . 10
class 𝑚 |
13 | 12 | cdm 5677 |
. . . . . . . . 9
class dom 𝑚 |
14 | 13 | cuni 4909 |
. . . . . . . 8
class ∪ dom 𝑚 |
15 | | cmap 8820 |
. . . . . . . 8
class
↑m |
16 | 11, 14, 15 | co 7409 |
. . . . . . 7
class (dom
𝑟 ↑m ∪ dom 𝑚) |
17 | 9, 16 | wcel 2107 |
. . . . . 6
wff 𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) |
18 | | vg |
. . . . . . . 8
setvar 𝑔 |
19 | 18 | cv 1541 |
. . . . . . 7
class 𝑔 |
20 | 19, 16 | wcel 2107 |
. . . . . 6
wff 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) |
21 | 17, 20 | wa 397 |
. . . . 5
wff (𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) |
22 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
23 | 22 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
24 | 23, 9 | cfv 6544 |
. . . . . . . 8
class (𝑓‘𝑥) |
25 | 23, 19 | cfv 6544 |
. . . . . . . 8
class (𝑔‘𝑥) |
26 | 24, 25, 10 | wbr 5149 |
. . . . . . 7
wff (𝑓‘𝑥)𝑟(𝑔‘𝑥) |
27 | 26, 22, 14 | crab 3433 |
. . . . . 6
class {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)} |
28 | | cae 33266 |
. . . . . 6
class
a.e. |
29 | 27, 12, 28 | wbr 5149 |
. . . . 5
wff {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚 |
30 | 21, 29 | wa 397 |
. . . 4
wff ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom
𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚) |
31 | 30, 8, 18 | copab 5211 |
. . 3
class
{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom
𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)} |
32 | 2, 3, 4, 7, 31 | cmpo 7411 |
. 2
class (𝑟 ∈ V, 𝑚 ∈ ∪ ran
measures ↦ {⟨𝑓,
𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom
𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)}) |
33 | 1, 32 | wceq 1542 |
1
wff ~ a.e. =
(𝑟 ∈ V, 𝑚 ∈ ∪ ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom
𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)}) |