This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )