Theorem toplatglb

Description: Greatest lower bounds in a topology are realized by the interior of the intersection. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	topclat.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
	toplatlub.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
	toplatlub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐽 )
	toplatglb.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
	toplatglb.e	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
Assertion	toplatglb	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = ( ( int ‘ 𝐽 ) ‘ ∩ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		topclat.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
2		toplatlub.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		toplatlub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐽 )
4		toplatglb.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
5		toplatglb.e	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
6	4	a1i	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐼 ) )
7		intssuni	⊢ ( 𝑆 ≠ ∅ → ∩ 𝑆 ⊆ ∪ 𝑆 )
8	5 7	syl	⊢ ( 𝜑 → ∩ 𝑆 ⊆ ∪ 𝑆 )
9	3	unissd	⊢ ( 𝜑 → ∪ 𝑆 ⊆ ∪ 𝐽 )
10	8 9	sstrd	⊢ ( 𝜑 → ∩ 𝑆 ⊆ ∪ 𝐽 )
11		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
12	11	ntrval	⊢ ( ( 𝐽 ∈ Top ∧ ∩ 𝑆 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ∩ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 ∩ 𝑆 ) )
13	2 10 12	syl2anc	⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∩ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 ∩ 𝑆 ) )
14	2	uniexd	⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
15	14 10	ssexd	⊢ ( 𝜑 → ∩ 𝑆 ∈ V )
16		inpw	⊢ ( ∩ 𝑆 ∈ V → ( 𝐽 ∩ 𝒫 ∩ 𝑆 ) = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ∩ 𝑆 } )
17	16	unieqd	⊢ ( ∩ 𝑆 ∈ V → ∪ ( 𝐽 ∩ 𝒫 ∩ 𝑆 ) = ∪ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ∩ 𝑆 } )
18	15 17	syl	⊢ ( 𝜑 → ∪ ( 𝐽 ∩ 𝒫 ∩ 𝑆 ) = ∪ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ∩ 𝑆 } )
19	13 18	eqtrd	⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∩ 𝑆 ) = ∪ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ∩ 𝑆 } )
20	11	ntropn	⊢ ( ( 𝐽 ∈ Top ∧ ∩ 𝑆 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ∩ 𝑆 ) ∈ 𝐽 )
21	2 10 20	syl2anc	⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∩ 𝑆 ) ∈ 𝐽 )
22	1 2 3 6 19 21	ipoglb	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = ( ( int ‘ 𝐽 ) ‘ ∩ 𝑆 ) )