toplatlub

Description: Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024)

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

Metamath Proof Explorer