Step |
Hyp |
Ref |
Expression |
0 |
|
cglb |
|- glb |
1 |
|
vp |
|- p |
2 |
|
cvv |
|- _V |
3 |
|
vs |
|- s |
4 |
|
cbs |
|- Base |
5 |
1
|
cv |
|- p |
6 |
5 4
|
cfv |
|- ( Base ` p ) |
7 |
6
|
cpw |
|- ~P ( Base ` p ) |
8 |
|
vx |
|- x |
9 |
|
vy |
|- y |
10 |
3
|
cv |
|- s |
11 |
8
|
cv |
|- x |
12 |
|
cple |
|- le |
13 |
5 12
|
cfv |
|- ( le ` p ) |
14 |
9
|
cv |
|- y |
15 |
11 14 13
|
wbr |
|- x ( le ` p ) y |
16 |
15 9 10
|
wral |
|- A. y e. s x ( le ` p ) y |
17 |
|
vz |
|- z |
18 |
17
|
cv |
|- z |
19 |
18 14 13
|
wbr |
|- z ( le ` p ) y |
20 |
19 9 10
|
wral |
|- A. y e. s z ( le ` p ) y |
21 |
18 11 13
|
wbr |
|- z ( le ` p ) x |
22 |
20 21
|
wi |
|- ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) |
23 |
22 17 6
|
wral |
|- A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) |
24 |
16 23
|
wa |
|- ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) |
25 |
24 8 6
|
crio |
|- ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) |
26 |
3 7 25
|
cmpt |
|- ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) ) |
27 |
24 8 6
|
wreu |
|- E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) |
28 |
27 3
|
cab |
|- { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) } |
29 |
26 28
|
cres |
|- ( ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) ) |` { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) } ) |
30 |
1 2 29
|
cmpt |
|- ( p e. _V |-> ( ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) ) |` { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) } ) ) |
31 |
0 30
|
wceq |
|- glb = ( p e. _V |-> ( ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) ) |` { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) } ) ) |