Step |
Hyp |
Ref |
Expression |
0 |
|
cocaN |
⊢ ocA |
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 |
|
cdia |
⊢ DIsoA |
14 |
5 13
|
cfv |
⊢ ( DIsoA ‘ 𝑘 ) |
15 |
10 14
|
cfv |
⊢ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) |
16 |
|
coc |
⊢ oc |
17 |
5 16
|
cfv |
⊢ ( oc ‘ 𝑘 ) |
18 |
15
|
ccnv |
⊢ ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) |
19 |
|
vz |
⊢ 𝑧 |
20 |
15
|
crn |
⊢ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) |
21 |
7
|
cv |
⊢ 𝑥 |
22 |
19
|
cv |
⊢ 𝑧 |
23 |
21 22
|
wss |
⊢ 𝑥 ⊆ 𝑧 |
24 |
23 19 20
|
crab |
⊢ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } |
25 |
24
|
cint |
⊢ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } |
26 |
25 18
|
cfv |
⊢ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) |
27 |
26 17
|
cfv |
⊢ ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) |
28 |
|
cjn |
⊢ join |
29 |
5 28
|
cfv |
⊢ ( join ‘ 𝑘 ) |
30 |
10 17
|
cfv |
⊢ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) |
31 |
27 30 29
|
co |
⊢ ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) |
32 |
|
cmee |
⊢ meet |
33 |
5 32
|
cfv |
⊢ ( meet ‘ 𝑘 ) |
34 |
31 10 33
|
co |
⊢ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) |
35 |
34 15
|
cfv |
⊢ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) |
36 |
7 12 35
|
cmpt |
⊢ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) |
37 |
3 6 36
|
cmpt |
⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) |
38 |
1 2 37
|
cmpt |
⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) |
39 |
0 38
|
wceq |
⊢ ocA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) |