| Step |
Hyp |
Ref |
Expression |
| 1 |
|
toplatmeet.i |
|- I = ( toInc ` J ) |
| 2 |
|
toplatmeet.j |
|- ( ph -> J e. Top ) |
| 3 |
|
toplatmeet.a |
|- ( ph -> A e. J ) |
| 4 |
|
toplatmeet.b |
|- ( ph -> B e. J ) |
| 5 |
|
toplatmeet.m |
|- ./\ = ( meet ` I ) |
| 6 |
|
eqid |
|- ( glb ` I ) = ( glb ` I ) |
| 7 |
1
|
ipopos |
|- I e. Poset |
| 8 |
7
|
a1i |
|- ( ph -> I e. Poset ) |
| 9 |
6 5 8 3 4
|
meetval |
|- ( ph -> ( A ./\ B ) = ( ( glb ` I ) ` { A , B } ) ) |
| 10 |
3 4
|
prssd |
|- ( ph -> { A , B } C_ J ) |
| 11 |
6
|
a1i |
|- ( ph -> ( glb ` I ) = ( glb ` I ) ) |
| 12 |
|
intprg |
|- ( ( A e. J /\ B e. J ) -> |^| { A , B } = ( A i^i B ) ) |
| 13 |
3 4 12
|
syl2anc |
|- ( ph -> |^| { A , B } = ( A i^i B ) ) |
| 14 |
|
inopn |
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J ) |
| 15 |
2 3 4 14
|
syl3anc |
|- ( ph -> ( A i^i B ) e. J ) |
| 16 |
13 15
|
eqeltrd |
|- ( ph -> |^| { A , B } e. J ) |
| 17 |
|
unimax |
|- ( |^| { A , B } e. J -> U. { x e. J | x C_ |^| { A , B } } = |^| { A , B } ) |
| 18 |
16 17
|
syl |
|- ( ph -> U. { x e. J | x C_ |^| { A , B } } = |^| { A , B } ) |
| 19 |
18 13
|
eqtr2d |
|- ( ph -> ( A i^i B ) = U. { x e. J | x C_ |^| { A , B } } ) |
| 20 |
1 2 10 11 19 15
|
ipoglb |
|- ( ph -> ( ( glb ` I ) ` { A , B } ) = ( A i^i B ) ) |
| 21 |
9 20
|
eqtrd |
|- ( ph -> ( A ./\ B ) = ( A i^i B ) ) |