Theorem toplatglb

Description: Greatest lower bounds in a topology are realized by the interior of the intersection. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	topclat.i	|- I = ( toInc ` J )
	toplatlub.j	|- ( ph -> J e. Top )
	toplatlub.s	|- ( ph -> S C_ J )
	toplatglb.g	|- G = ( glb ` I )
	toplatglb.e	|- ( ph -> S =/= (/) )
Assertion	toplatglb	|- ( ph -> ( G ` S ) = ( ( int ` J ) ` |^| S ) )

Proof

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 ) )