Step |
Hyp |
Ref |
Expression |
0 |
|
cmir |
⊢ pInvG |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvv |
⊢ V |
3 |
|
vm |
⊢ 𝑚 |
4 |
|
cbs |
⊢ Base |
5 |
1
|
cv |
⊢ 𝑔 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑔 ) |
7 |
|
va |
⊢ 𝑎 |
8 |
|
vb |
⊢ 𝑏 |
9 |
3
|
cv |
⊢ 𝑚 |
10 |
|
cds |
⊢ dist |
11 |
5 10
|
cfv |
⊢ ( dist ‘ 𝑔 ) |
12 |
8
|
cv |
⊢ 𝑏 |
13 |
9 12 11
|
co |
⊢ ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) |
14 |
7
|
cv |
⊢ 𝑎 |
15 |
9 14 11
|
co |
⊢ ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) |
16 |
13 15
|
wceq |
⊢ ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) |
17 |
|
citv |
⊢ Itv |
18 |
5 17
|
cfv |
⊢ ( Itv ‘ 𝑔 ) |
19 |
12 14 18
|
co |
⊢ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) |
20 |
9 19
|
wcel |
⊢ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) |
21 |
16 20
|
wa |
⊢ ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) |
22 |
21 8 6
|
crio |
⊢ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) |
23 |
7 6 22
|
cmpt |
⊢ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) |
24 |
3 6 23
|
cmpt |
⊢ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) |
25 |
1 2 24
|
cmpt |
⊢ ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) ) |
26 |
0 25
|
wceq |
⊢ pInvG = ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) ) |