Step |
Hyp |
Ref |
Expression |
0 |
|
cdjaN |
⊢ vA |
1 |
|
vk |
⊢ 𝑘 |
2 |
|
cvv |
⊢ V |
3 |
|
vw |
⊢ 𝑤 |
4 |
|
clh |
⊢ LHyp |
5 |
1
|
cv |
⊢ 𝑘 |
6 |
5 4
|
cfv |
⊢ ( LHyp ‘ 𝑘 ) |
7 |
|
vx |
⊢ 𝑥 |
8 |
|
cltrn |
⊢ LTrn |
9 |
5 8
|
cfv |
⊢ ( LTrn ‘ 𝑘 ) |
10 |
3
|
cv |
⊢ 𝑤 |
11 |
10 9
|
cfv |
⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) |
12 |
11
|
cpw |
⊢ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) |
13 |
|
vy |
⊢ 𝑦 |
14 |
|
cocaN |
⊢ ocA |
15 |
5 14
|
cfv |
⊢ ( ocA ‘ 𝑘 ) |
16 |
10 15
|
cfv |
⊢ ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) |
17 |
7
|
cv |
⊢ 𝑥 |
18 |
17 16
|
cfv |
⊢ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) |
19 |
13
|
cv |
⊢ 𝑦 |
20 |
19 16
|
cfv |
⊢ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) |
21 |
18 20
|
cin |
⊢ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) |
22 |
21 16
|
cfv |
⊢ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) |
23 |
7 13 12 12 22
|
cmpo |
⊢ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) |
24 |
3 6 23
|
cmpt |
⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) |
25 |
1 2 24
|
cmpt |
⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) ) |
26 |
0 25
|
wceq |
⊢ vA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑦 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) ∩ ( ( ( ocA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ) ) ) ) ) |