| Step |
Hyp |
Ref |
Expression |
| 1 |
|
topclat.i |
|- I = ( toInc ` J ) |
| 2 |
|
toplatlub.j |
|- ( ph -> J e. Top ) |
| 3 |
|
toplatlub.s |
|- ( ph -> S C_ J ) |
| 4 |
|
toplatglb.g |
|- G = ( glb ` I ) |
| 5 |
|
toplatglb.e |
|- ( ph -> S =/= (/) ) |
| 6 |
4
|
a1i |
|- ( ph -> G = ( glb ` I ) ) |
| 7 |
|
intssuni |
|- ( S =/= (/) -> |^| S C_ U. S ) |
| 8 |
5 7
|
syl |
|- ( ph -> |^| S C_ U. S ) |
| 9 |
3
|
unissd |
|- ( ph -> U. S C_ U. J ) |
| 10 |
8 9
|
sstrd |
|- ( ph -> |^| S C_ U. J ) |
| 11 |
|
eqid |
|- U. J = U. J |
| 12 |
11
|
ntrval |
|- ( ( J e. Top /\ |^| S C_ U. J ) -> ( ( int ` J ) ` |^| S ) = U. ( J i^i ~P |^| S ) ) |
| 13 |
2 10 12
|
syl2anc |
|- ( ph -> ( ( int ` J ) ` |^| S ) = U. ( J i^i ~P |^| S ) ) |
| 14 |
2
|
uniexd |
|- ( ph -> U. J e. _V ) |
| 15 |
14 10
|
ssexd |
|- ( ph -> |^| S e. _V ) |
| 16 |
|
inpw |
|- ( |^| S e. _V -> ( J i^i ~P |^| S ) = { x e. J | x C_ |^| S } ) |
| 17 |
16
|
unieqd |
|- ( |^| S e. _V -> U. ( J i^i ~P |^| S ) = U. { x e. J | x C_ |^| S } ) |
| 18 |
15 17
|
syl |
|- ( ph -> U. ( J i^i ~P |^| S ) = U. { x e. J | x C_ |^| S } ) |
| 19 |
13 18
|
eqtrd |
|- ( ph -> ( ( int ` J ) ` |^| S ) = U. { x e. J | x C_ |^| S } ) |
| 20 |
11
|
ntropn |
|- ( ( J e. Top /\ |^| S C_ U. J ) -> ( ( int ` J ) ` |^| S ) e. J ) |
| 21 |
2 10 20
|
syl2anc |
|- ( ph -> ( ( int ` J ) ` |^| S ) e. J ) |
| 22 |
1 2 3 6 19 21
|
ipoglb |
|- ( ph -> ( G ` S ) = ( ( int ` J ) ` |^| S ) ) |