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 e. Top -> I e. DLat )

Proof

Step Hyp Ref Expression
1 topdlat.i 
 |-  I = ( toInc ` J )
2 1 topclat 
 |-  ( J e. Top -> I e. CLat )
3 clatl 
 |-  ( I e. CLat -> I e. Lat )
4 2 3 syl 
 |-  ( J e. Top -> I e. Lat )
5 simpl 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> J e. Top )
6 simpr2 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> y e. ( Base ` I ) )
7 1 ipobas 
 |-  ( J e. Top -> J = ( Base ` I ) )
8 5 7 syl 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> J = ( Base ` I ) )
9 6 8 eleqtrrd 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> y e. J )
10 simpr3 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> z e. ( Base ` I ) )
11 10 8 eleqtrrd 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> z e. J )
12 eqid 
 |-  ( join ` I ) = ( join ` I )
13 1 5 9 11 12 toplatjoin 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( y ( join ` I ) z ) = ( y u. z ) )
14 13 oveq2d 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x ( meet ` I ) ( y ( join ` I ) z ) ) = ( x ( meet ` I ) ( y u. z ) ) )
15 simpr1 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> x e. ( Base ` I ) )
16 15 8 eleqtrrd 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> x e. J )
17 unopn 
 |-  ( ( J e. Top /\ y e. J /\ z e. J ) -> ( y u. z ) e. J )
18 5 9 11 17 syl3anc 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( y u. z ) e. J )
19 eqid 
 |-  ( meet ` I ) = ( meet ` I )
20 1 5 16 18 19 toplatmeet 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x ( meet ` I ) ( y u. z ) ) = ( x i^i ( y u. z ) ) )
21 inopn 
 |-  ( ( J e. Top /\ x e. J /\ y e. J ) -> ( x i^i y ) e. J )
22 5 16 9 21 syl3anc 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x i^i y ) e. J )
23 inopn 
 |-  ( ( J e. Top /\ x e. J /\ z e. J ) -> ( x i^i z ) e. J )
24 5 16 11 23 syl3anc 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x i^i z ) e. J )
25 1 5 22 24 12 toplatjoin 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( ( x i^i y ) ( join ` I ) ( x i^i z ) ) = ( ( x i^i y ) u. ( x i^i z ) ) )
26 1 5 16 9 19 toplatmeet 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x ( meet ` I ) y ) = ( x i^i y ) )
27 1 5 16 11 19 toplatmeet 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x ( meet ` I ) z ) = ( x i^i z ) )
28 26 27 oveq12d 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( ( x ( meet ` I ) y ) ( join ` I ) ( x ( meet ` I ) z ) ) = ( ( x i^i y ) ( join ` I ) ( x i^i z ) ) )
29 indi 
 |-  ( x i^i ( y u. z ) ) = ( ( x i^i y ) u. ( x i^i z ) )
30 29 a1i 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x i^i ( y u. z ) ) = ( ( x i^i y ) u. ( x i^i z ) ) )
31 25 28 30 3eqtr4rd 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x i^i ( y u. z ) ) = ( ( x ( meet ` I ) y ) ( join ` I ) ( x ( meet ` I ) z ) ) )
32 14 20 31 3eqtrd 
 |-  ( ( J e. Top /\ ( x e. ( Base ` I ) /\ y e. ( Base ` I ) /\ z e. ( Base ` I ) ) ) -> ( x ( meet ` I ) ( y ( join ` I ) z ) ) = ( ( x ( meet ` I ) y ) ( join ` I ) ( x ( meet ` I ) z ) ) )
33 32 ralrimivvva 
 |-  ( J e. Top -> A. x e. ( Base ` I ) A. y e. ( Base ` I ) A. z e. ( 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 e. DLat <-> ( I e. Lat /\ A. x e. ( Base ` I ) A. y e. ( Base ` I ) A. z e. ( 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 e. Top -> I e. DLat )