Detailed syntax breakdown of Definition df-doch
Step | Hyp | Ref
| Expression |
1 | | coch 39098 |
. 2
class
ocH |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar 𝑤 |
5 | 2 | cv 1542 |
. . . . 5
class 𝑘 |
6 | | clh 37735 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6380 |
. . . 4
class
(LHyp‘𝑘) |
8 | | vx |
. . . . 5
setvar 𝑥 |
9 | 4 | cv 1542 |
. . . . . . . 8
class 𝑤 |
10 | | cdvh 38829 |
. . . . . . . . 9
class
DVecH |
11 | 5, 10 | cfv 6380 |
. . . . . . . 8
class
(DVecH‘𝑘) |
12 | 9, 11 | cfv 6380 |
. . . . . . 7
class
((DVecH‘𝑘)‘𝑤) |
13 | | cbs 16760 |
. . . . . . 7
class
Base |
14 | 12, 13 | cfv 6380 |
. . . . . 6
class
(Base‘((DVecH‘𝑘)‘𝑤)) |
15 | 14 | cpw 4513 |
. . . . 5
class 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) |
16 | 8 | cv 1542 |
. . . . . . . . . 10
class 𝑥 |
17 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
18 | 17 | cv 1542 |
. . . . . . . . . . 11
class 𝑦 |
19 | | cdih 38979 |
. . . . . . . . . . . . 13
class
DIsoH |
20 | 5, 19 | cfv 6380 |
. . . . . . . . . . . 12
class
(DIsoH‘𝑘) |
21 | 9, 20 | cfv 6380 |
. . . . . . . . . . 11
class
((DIsoH‘𝑘)‘𝑤) |
22 | 18, 21 | cfv 6380 |
. . . . . . . . . 10
class
(((DIsoH‘𝑘)‘𝑤)‘𝑦) |
23 | 16, 22 | wss 3866 |
. . . . . . . . 9
wff 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦) |
24 | 5, 13 | cfv 6380 |
. . . . . . . . 9
class
(Base‘𝑘) |
25 | 23, 17, 24 | crab 3065 |
. . . . . . . 8
class {𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)} |
26 | | cglb 17817 |
. . . . . . . . 9
class
glb |
27 | 5, 26 | cfv 6380 |
. . . . . . . 8
class
(glb‘𝑘) |
28 | 25, 27 | cfv 6380 |
. . . . . . 7
class
((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}) |
29 | | coc 16810 |
. . . . . . . 8
class
oc |
30 | 5, 29 | cfv 6380 |
. . . . . . 7
class
(oc‘𝑘) |
31 | 28, 30 | cfv 6380 |
. . . . . 6
class
((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})) |
32 | 31, 21 | cfv 6380 |
. . . . 5
class
(((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))) |
33 | 8, 15, 32 | cmpt 5135 |
. . . 4
class (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))) |
34 | 4, 7, 33 | cmpt 5135 |
. . 3
class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)}))))) |
35 | 2, 3, 34 | cmpt 5135 |
. 2
class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))) |
36 | 1, 35 | wceq 1543 |
1
wff ocH =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))) |