Theorem toplatglb0

Description: The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	topclat.i	|- I = ( toInc ` J )
	toplatlub.j	|- ( ph -> J e. Top )
	toplatglb0.g	|- G = ( glb ` I )
Assertion	toplatglb0	|- ( ph -> ( G ` (/) ) = U. J )

Proof

Step	Hyp	Ref	Expression
1		topclat.i	|- I = ( toInc ` J )
2		toplatlub.j	|- ( ph -> J e. Top )
3		toplatglb0.g	|- G = ( glb ` I )
4	3	a1i	|- ( ph -> G = ( glb ` I ) )
5		eqid	|- U. J = U. J
6	5	topopn	|- ( J e. Top -> U. J e. J )
7	2 6	syl	|- ( ph -> U. J e. J )
8	1 4 7	ipoglb0	|- ( ph -> ( G ` (/) ) = U. J )