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 ⊢ 𝐼 = ( toInc ‘ 𝐽 )
Assertion topdlat ( 𝐽 ∈ Top → 𝐼 ∈ DLat )

Proof

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