| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lubpr.k |
|- ( ph -> K e. Poset ) |
| 2 |
|
lubpr.b |
|- B = ( Base ` K ) |
| 3 |
|
lubpr.x |
|- ( ph -> X e. B ) |
| 4 |
|
lubpr.y |
|- ( ph -> Y e. B ) |
| 5 |
|
lubpr.l |
|- .<_ = ( le ` K ) |
| 6 |
|
lubpr.c |
|- ( ph -> X .<_ Y ) |
| 7 |
|
lubpr.s |
|- ( ph -> S = { X , Y } ) |
| 8 |
|
glbpr.g |
|- G = ( glb ` K ) |
| 9 |
|
eqid |
|- ( ODual ` K ) = ( ODual ` K ) |
| 10 |
9
|
odupos |
|- ( K e. Poset -> ( ODual ` K ) e. Poset ) |
| 11 |
1 10
|
syl |
|- ( ph -> ( ODual ` K ) e. Poset ) |
| 12 |
9 2
|
odubas |
|- B = ( Base ` ( ODual ` K ) ) |
| 13 |
9 5
|
oduleval |
|- `' .<_ = ( le ` ( ODual ` K ) ) |
| 14 |
|
brcnvg |
|- ( ( Y e. B /\ X e. B ) -> ( Y `' .<_ X <-> X .<_ Y ) ) |
| 15 |
4 3 14
|
syl2anc |
|- ( ph -> ( Y `' .<_ X <-> X .<_ Y ) ) |
| 16 |
6 15
|
mpbird |
|- ( ph -> Y `' .<_ X ) |
| 17 |
|
prcom |
|- { X , Y } = { Y , X } |
| 18 |
7 17
|
eqtrdi |
|- ( ph -> S = { Y , X } ) |
| 19 |
|
eqid |
|- ( lub ` ( ODual ` K ) ) = ( lub ` ( ODual ` K ) ) |
| 20 |
11 12 4 3 13 16 18 19
|
lubprdm |
|- ( ph -> S e. dom ( lub ` ( ODual ` K ) ) ) |
| 21 |
9 8
|
odulub |
|- ( K e. Poset -> G = ( lub ` ( ODual ` K ) ) ) |
| 22 |
1 21
|
syl |
|- ( ph -> G = ( lub ` ( ODual ` K ) ) ) |
| 23 |
22
|
dmeqd |
|- ( ph -> dom G = dom ( lub ` ( ODual ` K ) ) ) |
| 24 |
20 23
|
eleqtrrd |
|- ( ph -> S e. dom G ) |
| 25 |
22
|
fveq1d |
|- ( ph -> ( G ` S ) = ( ( lub ` ( ODual ` K ) ) ` S ) ) |
| 26 |
11 12 4 3 13 16 18 19
|
lubpr |
|- ( ph -> ( ( lub ` ( ODual ` K ) ) ` S ) = X ) |
| 27 |
25 26
|
eqtrd |
|- ( ph -> ( G ` S ) = X ) |
| 28 |
24 27
|
jca |
|- ( ph -> ( S e. dom G /\ ( G ` S ) = X ) ) |