Step |
Hyp |
Ref |
Expression |
0 |
|
cfae |
⊢ ~ a.e. |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
cvv |
⊢ V |
3 |
|
vm |
⊢ 𝑚 |
4 |
|
cmeas |
⊢ measures |
5 |
4
|
crn |
⊢ ran measures |
6 |
5
|
cuni |
⊢ ∪ ran measures |
7 |
|
vf |
⊢ 𝑓 |
8 |
|
vg |
⊢ 𝑔 |
9 |
7
|
cv |
⊢ 𝑓 |
10 |
1
|
cv |
⊢ 𝑟 |
11 |
10
|
cdm |
⊢ dom 𝑟 |
12 |
|
cmap |
⊢ ↑m |
13 |
3
|
cv |
⊢ 𝑚 |
14 |
13
|
cdm |
⊢ dom 𝑚 |
15 |
14
|
cuni |
⊢ ∪ dom 𝑚 |
16 |
11 15 12
|
co |
⊢ ( dom 𝑟 ↑m ∪ dom 𝑚 ) |
17 |
9 16
|
wcel |
⊢ 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) |
18 |
8
|
cv |
⊢ 𝑔 |
19 |
18 16
|
wcel |
⊢ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) |
20 |
17 19
|
wa |
⊢ ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) |
21 |
|
vx |
⊢ 𝑥 |
22 |
21
|
cv |
⊢ 𝑥 |
23 |
22 9
|
cfv |
⊢ ( 𝑓 ‘ 𝑥 ) |
24 |
22 18
|
cfv |
⊢ ( 𝑔 ‘ 𝑥 ) |
25 |
23 24 10
|
wbr |
⊢ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) |
26 |
25 21 15
|
crab |
⊢ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } |
27 |
|
cae |
⊢ a.e. |
28 |
26 13 27
|
wbr |
⊢ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 |
29 |
20 28
|
wa |
⊢ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) |
30 |
29 7 8
|
copab |
⊢ { 〈 𝑓 , 𝑔 〉 ∣ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) } |
31 |
1 3 2 6 30
|
cmpo |
⊢ ( 𝑟 ∈ V , 𝑚 ∈ ∪ ran measures ↦ { 〈 𝑓 , 𝑔 〉 ∣ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) } ) |
32 |
0 31
|
wceq |
⊢ ~ a.e. = ( 𝑟 ∈ V , 𝑚 ∈ ∪ ran measures ↦ { 〈 𝑓 , 𝑔 〉 ∣ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) } ) |