Theorem topclat

Description: A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypothesis	topclat.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
Assertion	topclat	⊢ ( 𝐽 ∈ Top → 𝐼 ∈ CLat )

Proof

Step	Hyp	Ref	Expression
1		topclat.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
2	1	ipobas	⊢ ( 𝐽 ∈ Top → 𝐽 = ( Base ‘ 𝐼 ) )
3		eqidd	⊢ ( 𝐽 ∈ Top → ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 ) )
4		eqidd	⊢ ( 𝐽 ∈ Top → ( glb ‘ 𝐼 ) = ( glb ‘ 𝐼 ) )
5	1	ipopos	⊢ 𝐼 ∈ Poset
6	5	a1i	⊢ ( 𝐽 ∈ Top → 𝐼 ∈ Poset )
7		uniopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ∪ 𝑥 ∈ 𝐽 )
8		simpl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → 𝐽 ∈ Top )
9		simpr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → 𝑥 ⊆ 𝐽 )
10		eqidd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 ) )
11		intmin	⊢ ( ∪ 𝑥 ∈ 𝐽 → ∩ { 𝑦 ∈ 𝐽 ∣ ∪ 𝑥 ⊆ 𝑦 } = ∪ 𝑥 )
12	11	eqcomd	⊢ ( ∪ 𝑥 ∈ 𝐽 → ∪ 𝑥 = ∩ { 𝑦 ∈ 𝐽 ∣ ∪ 𝑥 ⊆ 𝑦 } )
13	7 12	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ∪ 𝑥 = ∩ { 𝑦 ∈ 𝐽 ∣ ∪ 𝑥 ⊆ 𝑦 } )
14	1 8 9 10 13	ipolubdm	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ( 𝑥 ∈ dom ( lub ‘ 𝐼 ) ↔ ∪ 𝑥 ∈ 𝐽 ) )
15	7 14	mpbird	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → 𝑥 ∈ dom ( lub ‘ 𝐼 ) )
16		ssrab2	⊢ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ∩ 𝑥 } ⊆ 𝐽
17		uniopn	⊢ ( ( 𝐽 ∈ Top ∧ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ∩ 𝑥 } ⊆ 𝐽 ) → ∪ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐽 )
18	8 16 17	sylancl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ∪ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐽 )
19		eqidd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ( glb ‘ 𝐼 ) = ( glb ‘ 𝐼 ) )
20		eqidd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ∪ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ∩ 𝑥 } = ∪ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ∩ 𝑥 } )
21	1 8 9 19 20	ipoglbdm	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → ( 𝑥 ∈ dom ( glb ‘ 𝐼 ) ↔ ∪ { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐽 ) )
22	18 21	mpbird	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝐽 ) → 𝑥 ∈ dom ( glb ‘ 𝐼 ) )
23	2 3 4 6 15 22	isclatd	⊢ ( 𝐽 ∈ Top → 𝐼 ∈ CLat )