Metamath Proof Explorer

Theorem toslat

Description: A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Assertion toslat 
|- ( K e. Toset -> K e. Lat )

Proof

Step Hyp Ref Expression
1 tospos 
 |-  ( K e. Toset -> K e. Poset )
2 1 ad2antrr 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ x ( le ` K ) y ) -> K e. Poset )
3 eqid 
 |-  ( Base ` K ) = ( Base ` K )
4 simplrl 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ x ( le ` K ) y ) -> x e. ( Base ` K ) )
5 simplrr 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ x ( le ` K ) y ) -> y e. ( Base ` K ) )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 simpr 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ x ( le ` K ) y ) -> x ( le ` K ) y )
8 eqidd 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ x ( le ` K ) y ) -> { x , y } = { x , y } )
9 eqid 
 |-  ( lub ` K ) = ( lub ` K )
10 2 3 4 5 6 7 8 9 lubprdm 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ x ( le ` K ) y ) -> { x , y } e. dom ( lub ` K ) )
11 1 ad2antrr 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ y ( le ` K ) x ) -> K e. Poset )
12 simplrr 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ y ( le ` K ) x ) -> y e. ( Base ` K ) )
13 simplrl 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ y ( le ` K ) x ) -> x e. ( Base ` K ) )
14 simpr 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ y ( le ` K ) x ) -> y ( le ` K ) x )
15 prcom 
 |-  { x , y } = { y , x }
16 15 a1i 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ y ( le ` K ) x ) -> { x , y } = { y , x } )
17 11 3 12 13 6 14 16 9 lubprdm 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ y ( le ` K ) x ) -> { x , y } e. dom ( lub ` K ) )
18 3 6 tleile 
 |-  ( ( K e. Toset /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x ( le ` K ) y \/ y ( le ` K ) x ) )
19 18 3expb 
 |-  ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( le ` K ) y \/ y ( le ` K ) x ) )
20 10 17 19 mpjaodan 
 |-  ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> { x , y } e. dom ( lub ` K ) )
21 20 ralrimivva 
 |-  ( K e. Toset -> A. x e. ( Base ` K ) A. y e. ( Base ` K ) { x , y } e. dom ( lub ` K ) )
22 eqid 
 |-  ( join ` K ) = ( join ` K )
23 3 1 9 22 joindm2 
 |-  ( K e. Toset -> ( dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) { x , y } e. dom ( lub ` K ) ) )
24 21 23 mpbird 
 |-  ( K e. Toset -> dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) )
25 eqid 
 |-  ( glb ` K ) = ( glb ` K )
26 2 3 4 5 6 7 8 25 glbprdm 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ x ( le ` K ) y ) -> { x , y } e. dom ( glb ` K ) )
27 11 3 12 13 6 14 16 25 glbprdm 
 |-  ( ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) /\ y ( le ` K ) x ) -> { x , y } e. dom ( glb ` K ) )
28 26 27 19 mpjaodan 
 |-  ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> { x , y } e. dom ( glb ` K ) )
29 28 ralrimivva 
 |-  ( K e. Toset -> A. x e. ( Base ` K ) A. y e. ( Base ` K ) { x , y } e. dom ( glb ` K ) )
30 eqid 
 |-  ( meet ` K ) = ( meet ` K )
31 3 1 25 30 meetdm2 
 |-  ( K e. Toset -> ( dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) <-> A. x e. ( Base ` K ) A. y e. ( Base ` K ) { x , y } e. dom ( glb ` K ) ) )
32 29 31 mpbird 
 |-  ( K e. Toset -> dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) )
33 24 32 jca 
 |-  ( K e. Toset -> ( dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) /\ dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) )
34 3 22 30 islat 
 |-  ( K e. Lat <-> ( K e. Poset /\ ( dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) /\ dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
35 1 33 34 sylanbrc 
 |-  ( K e. Toset -> K e. Lat )