Metamath Proof Explorer

Theorem toslat

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

Ref Expression
Assertion toslat ( 𝐾 ∈ Toset → 𝐾 ∈ Lat )

Proof

Step Hyp Ref Expression
1 tospos ⊢ ( 𝐾 ∈ Toset → 𝐾 ∈ Poset )
2 1 ad2antrr ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) → 𝐾 ∈ Poset )
3 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 simplrl ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
5 simplrr ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
6 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 simpr ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) → 𝑥 ( le ‘ 𝐾 ) 𝑦 )
8 eqidd ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) → { 𝑥 , 𝑦 } = { 𝑥 , 𝑦 } )
9 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
10 2 3 4 5 6 7 8 9 lubprdm ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) → { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) )
11 1 ad2antrr ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝐾 ∈ Poset )
12 simplrr ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
13 simplrl ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
14 simpr ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑦 ( le ‘ 𝐾 ) 𝑥 )
15 prcom ⊢ { 𝑥 , 𝑦 } = { 𝑦 , 𝑥 }
16 15 a1i ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → { 𝑥 , 𝑦 } = { 𝑦 , 𝑥 } )
17 11 3 12 13 6 14 16 9 lubprdm ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) )
18 3 6 tleile ⊢ ( ( 𝐾 ∈ Toset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
19 18 3expb ⊢ ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
20 10 17 19 mpjaodan ⊢ ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) )
21 20 ralrimivva ⊢ ( 𝐾 ∈ Toset → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) )
22 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
23 3 1 9 22 joindm2 ⊢ ( 𝐾 ∈ Toset → ( dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) )
24 21 23 mpbird ⊢ ( 𝐾 ∈ Toset → dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
25 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
26 2 3 4 5 6 7 8 25 glbprdm ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) → { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) )
27 11 3 12 13 6 14 16 25 glbprdm ⊢ ( ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) )
28 26 27 19 mpjaodan ⊢ ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) )
29 28 ralrimivva ⊢ ( 𝐾 ∈ Toset → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) )
30 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
31 3 1 25 30 meetdm2 ⊢ ( 𝐾 ∈ Toset → ( dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) )
32 29 31 mpbird ⊢ ( 𝐾 ∈ Toset → dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
33 24 32 jca ⊢ ( 𝐾 ∈ Toset → ( dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∧ dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
34 3 22 30 islat ⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∧ dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
35 1 33 34 sylanbrc ⊢ ( 𝐾 ∈ Toset → 𝐾 ∈ Lat )