| Step |
Hyp |
Ref |
Expression |
| 1 |
|
poslubdg.l |
|- .<_ = ( le ` K ) |
| 2 |
|
poslubdg.b |
|- ( ph -> B = ( Base ` K ) ) |
| 3 |
|
poslubdg.u |
|- ( ph -> U = ( lub ` K ) ) |
| 4 |
|
poslubdg.k |
|- ( ph -> K e. Poset ) |
| 5 |
|
poslubdg.s |
|- ( ph -> S C_ B ) |
| 6 |
|
poslubdg.t |
|- ( ph -> T e. B ) |
| 7 |
|
poslubdg.ub |
|- ( ( ph /\ x e. S ) -> x .<_ T ) |
| 8 |
|
poslubdg.le |
|- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y ) |
| 9 |
3
|
fveq1d |
|- ( ph -> ( U ` S ) = ( ( lub ` K ) ` S ) ) |
| 10 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
| 11 |
|
eqid |
|- ( lub ` K ) = ( lub ` K ) |
| 12 |
5 2
|
sseqtrd |
|- ( ph -> S C_ ( Base ` K ) ) |
| 13 |
6 2
|
eleqtrd |
|- ( ph -> T e. ( Base ` K ) ) |
| 14 |
2
|
eleq2d |
|- ( ph -> ( y e. B <-> y e. ( Base ` K ) ) ) |
| 15 |
14
|
biimpar |
|- ( ( ph /\ y e. ( Base ` K ) ) -> y e. B ) |
| 16 |
15
|
3adant3 |
|- ( ( ph /\ y e. ( Base ` K ) /\ A. x e. S x .<_ y ) -> y e. B ) |
| 17 |
16 8
|
syld3an2 |
|- ( ( ph /\ y e. ( Base ` K ) /\ A. x e. S x .<_ y ) -> T .<_ y ) |
| 18 |
1 10 11 4 12 13 7 17
|
poslubd |
|- ( ph -> ( ( lub ` K ) ` S ) = T ) |
| 19 |
9 18
|
eqtrd |
|- ( ph -> ( U ` S ) = T ) |