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	⊢ 𝐼 = ( toInc ‘ 𝐽 )
	toplatlub.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
	toplatlub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐽 )
	toplatlub.u	⊢ 𝑈 = ( lub ‘ 𝐼 )
Assertion	toplatlub	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ∪ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		topclat.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
2		toplatlub.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		toplatlub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐽 )
4		toplatlub.u	⊢ 𝑈 = ( lub ‘ 𝐼 )
5	4	a1i	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
6		uniopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝐽 ) → ∪ 𝑆 ∈ 𝐽 )
7	2 3 6	syl2anc	⊢ ( 𝜑 → ∪ 𝑆 ∈ 𝐽 )
8		intmin	⊢ ( ∪ 𝑆 ∈ 𝐽 → ∩ { 𝑥 ∈ 𝐽 ∣ ∪ 𝑆 ⊆ 𝑥 } = ∪ 𝑆 )
9	8	eqcomd	⊢ ( ∪ 𝑆 ∈ 𝐽 → ∪ 𝑆 = ∩ { 𝑥 ∈ 𝐽 ∣ ∪ 𝑆 ⊆ 𝑥 } )
10	7 9	syl	⊢ ( 𝜑 → ∪ 𝑆 = ∩ { 𝑥 ∈ 𝐽 ∣ ∪ 𝑆 ⊆ 𝑥 } )
11	1 2 3 5 10 7	ipolub	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ∪ 𝑆 )