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 ⊢ I = toInc ⁡ J
Assertion topclat ⊢ J ∈ Top → I ∈ CLat

Proof

Step Hyp Ref Expression
1 topclat.i ⊢ I = toInc ⁡ J
2 1 ipobas ⊢ J ∈ Top → J = Base I
3 eqidd ⊢ J ∈ Top → lub ⁡ I = lub ⁡ I
4 eqidd ⊢ J ∈ Top → glb ⁡ I = glb ⁡ I
5 1 ipopos ⊢ I ∈ Poset
6 5 a1i ⊢ J ∈ Top → I ∈ Poset
7 uniopn ⊢ J ∈ Top ∧ x ⊆ J → ⋃ x ∈ J
8 simpl ⊢ J ∈ Top ∧ x ⊆ J → J ∈ Top
9 simpr ⊢ J ∈ Top ∧ x ⊆ J → x ⊆ J
10 eqidd ⊢ J ∈ Top ∧ x ⊆ J → lub ⁡ I = lub ⁡ I
11 intmin ⊢ ⋃ x ∈ J → ⋂ y ∈ J | ⋃ x ⊆ y = ⋃ x
12 11 eqcomd ⊢ ⋃ x ∈ J → ⋃ x = ⋂ y ∈ J | ⋃ x ⊆ y
13 7 12 syl ⊢ J ∈ Top ∧ x ⊆ J → ⋃ x = ⋂ y ∈ J | ⋃ x ⊆ y
14 1 8 9 10 13 ipolubdm ⊢ J ∈ Top ∧ x ⊆ J → x ∈ dom ⁡ lub ⁡ I ↔ ⋃ x ∈ J
15 7 14 mpbird ⊢ J ∈ Top ∧ x ⊆ J → x ∈ dom ⁡ lub ⁡ I
16 ssrab2 ⊢ y ∈ J | y ⊆ ⋂ x ⊆ J
17 uniopn ⊢ J ∈ Top ∧ y ∈ J | y ⊆ ⋂ x ⊆ J → ⋃ y ∈ J | y ⊆ ⋂ x ∈ J
18 8 16 17 sylancl ⊢ J ∈ Top ∧ x ⊆ J → ⋃ y ∈ J | y ⊆ ⋂ x ∈ J
19 eqidd ⊢ J ∈ Top ∧ x ⊆ J → glb ⁡ I = glb ⁡ I
20 eqidd ⊢ J ∈ Top ∧ x ⊆ J → ⋃ y ∈ J | y ⊆ ⋂ x = ⋃ y ∈ J | y ⊆ ⋂ x
21 1 8 9 19 20 ipoglbdm ⊢ J ∈ Top ∧ x ⊆ J → x ∈ dom ⁡ glb ⁡ I ↔ ⋃ y ∈ J | y ⊆ ⋂ x ∈ J
22 18 21 mpbird ⊢ J ∈ Top ∧ x ⊆ J → x ∈ dom ⁡ glb ⁡ I
23 2 3 4 6 15 22 isclatd ⊢ J ∈ Top → I ∈ CLat