Metamath Proof Explorer

Theorem topdlat

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

Ref Expression
Hypothesis topdlat.i ⊢ I = toInc ⁡ J
Assertion topdlat ⊢ J ∈ Top → I ∈ DLat

Proof

Step Hyp Ref Expression
1 topdlat.i ⊢ I = toInc ⁡ J
2 1 topclat ⊢ J ∈ Top → I ∈ CLat
3 clatl ⊢ I ∈ CLat → I ∈ Lat
4 2 3 syl ⊢ J ∈ Top → I ∈ Lat
5 simpl ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → J ∈ Top
6 simpr2 ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → y ∈ Base I
7 1 ipobas ⊢ J ∈ Top → J = Base I
8 5 7 syl ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → J = Base I
9 6 8 eleqtrrd ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → y ∈ J
10 simpr3 ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → z ∈ Base I
11 10 8 eleqtrrd ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → z ∈ J
12 eqid ⊢ join ⁡ I = join ⁡ I
13 1 5 9 11 12 toplatjoin ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → y join ⁡ I z = y ∪ z
14 13 oveq2d ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x meet ⁡ I y join ⁡ I z = x meet ⁡ I y ∪ z
15 simpr1 ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x ∈ Base I
16 15 8 eleqtrrd ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x ∈ J
17 unopn ⊢ J ∈ Top ∧ y ∈ J ∧ z ∈ J → y ∪ z ∈ J
18 5 9 11 17 syl3anc ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → y ∪ z ∈ J
19 eqid ⊢ meet ⁡ I = meet ⁡ I
20 1 5 16 18 19 toplatmeet ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x meet ⁡ I y ∪ z = x ∩ y ∪ z
21 inopn ⊢ J ∈ Top ∧ x ∈ J ∧ y ∈ J → x ∩ y ∈ J
22 5 16 9 21 syl3anc ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x ∩ y ∈ J
23 inopn ⊢ J ∈ Top ∧ x ∈ J ∧ z ∈ J → x ∩ z ∈ J
24 5 16 11 23 syl3anc ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x ∩ z ∈ J
25 1 5 22 24 12 toplatjoin ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x ∩ y join ⁡ I x ∩ z = x ∩ y ∪ x ∩ z
26 1 5 16 9 19 toplatmeet ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x meet ⁡ I y = x ∩ y
27 1 5 16 11 19 toplatmeet ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x meet ⁡ I z = x ∩ z
28 26 27 oveq12d ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x meet ⁡ I y join ⁡ I x meet ⁡ I z = x ∩ y join ⁡ I x ∩ z
29 indi ⊢ x ∩ y ∪ z = x ∩ y ∪ x ∩ z
30 29 a1i ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x ∩ y ∪ z = x ∩ y ∪ x ∩ z
31 25 28 30 3eqtr4rd ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x ∩ y ∪ z = x meet ⁡ I y join ⁡ I x meet ⁡ I z
32 14 20 31 3eqtrd ⊢ J ∈ Top ∧ x ∈ Base I ∧ y ∈ Base I ∧ z ∈ Base I → x meet ⁡ I y join ⁡ I z = x meet ⁡ I y join ⁡ I x meet ⁡ I z
33 32 ralrimivvva ⊢ J ∈ Top → ∀ x ∈ Base I ∀ y ∈ Base I ∀ z ∈ Base I x meet ⁡ I y join ⁡ I z = x meet ⁡ I y join ⁡ I x meet ⁡ I z
34 eqid ⊢ Base I = Base I
35 34 12 19 isdlat ⊢ I ∈ DLat ↔ I ∈ Lat ∧ ∀ x ∈ Base I ∀ y ∈ Base I ∀ z ∈ Base I x meet ⁡ I y join ⁡ I z = x meet ⁡ I y join ⁡ I x meet ⁡ I z
36 4 33 35 sylanbrc ⊢ J ∈ Top → I ∈ DLat