Theorem toplatlub

Description: Least upper bounds in a topology are realized by unions. (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 )
	toplatlub.u	|- U = ( lub ` I )
Assertion	toplatlub	|- ( ph -> ( U ` S ) = U. 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		toplatlub.u	|- U = ( lub ` I )
5	4	a1i	|- ( ph -> U = ( lub ` I ) )
6		uniopn	|- ( ( J e. Top /\ S C_ J ) -> U. S e. J )
7	2 3 6	syl2anc	|- ( ph -> U. S e. J )
8		intmin	|- ( U. S e. J -> |^| { x e. J | U. S C_ x } = U. S )
9	8	eqcomd	|- ( U. S e. J -> U. S = |^| { x e. J | U. S C_ x } )
10	7 9	syl	|- ( ph -> U. S = |^| { x e. J | U. S C_ x } )
11	1 2 3 5 10 7	ipolub	|- ( ph -> ( U ` S ) = U. S )