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=\mathrm{toInc}\left(J\right)$$
	toplatlub.j	$$⊢\phi \to J\in \mathrm{Top}$$
	toplatlub.s	$$⊢\phi \to S\subseteq J$$
	toplatlub.u	$$⊢U=\mathrm{lub}\left(I\right)$$
Assertion	toplatlub	$$⊢\phi \to U\left(S\right)=\bigcup S$$

Proof

Step	Hyp	Ref	Expression
1		topclat.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
2		toplatlub.j	$$⊢\phi \to J\in \mathrm{Top}$$
3		toplatlub.s	$$⊢\phi \to S\subseteq J$$
4		toplatlub.u	$$⊢U=\mathrm{lub}\left(I\right)$$
5	4	a1i	$$⊢\phi \to U=\mathrm{lub}\left(I\right)$$
6		uniopn	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq J\right)\to \bigcup S\in J$$
7	2 3 6	syl2anc	$$⊢\phi \to \bigcup S\in J$$
8		intmin	$$⊢\bigcup S\in J\to \bigcap \left\{x\in J|\bigcup S\subseteq x\right\}=\bigcup S$$
9	8	eqcomd	$$⊢\bigcup S\in J\to \bigcup S=\bigcap \left\{x\in J|\bigcup S\subseteq x\right\}$$
10	7 9	syl	$$⊢\phi \to \bigcup S=\bigcap \left\{x\in J|\bigcup S\subseteq x\right\}$$
11	1 2 3 5 10 7	ipolub	$$⊢\phi \to U\left(S\right)=\bigcup S$$