Metamath Proof Explorer

Theorem clatl

Description: A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011) TODO: use eqrelrdv2 to shorten proof and eliminate joindmss and meetdmss ?

Ref Expression
Assertion clatl ( 𝐾 ∈ CLat → 𝐾 ∈ Lat )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
3 simpl ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → 𝐾 ∈ Poset )
4 1 2 3 joindmss ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → dom ( join ‘ 𝐾 ) ⊆ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
5 relxp ⊢ Rel ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) )
6 5 a1i ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → Rel ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
7 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) )
8 vex ⊢ 𝑥 ∈ V
9 vex ⊢ 𝑦 ∈ V
10 8 9 prss ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ↔ { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) )
11 7 10 sylbb ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) )
12 prex ⊢ { 𝑥 , 𝑦 } ∈ V
13 12 elpw ⊢ ( { 𝑥 , 𝑦 } ∈ 𝒫 ( Base ‘ 𝐾 ) ↔ { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝐾 ) )
14 11 13 sylibr ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ∈ 𝒫 ( Base ‘ 𝐾 ) )
15 eleq2 ⊢ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) → ( { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ↔ { 𝑥 , 𝑦 } ∈ 𝒫 ( Base ‘ 𝐾 ) ) )
16 14 15 syl5ibr ⊢ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) )
17 16 adantl ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) )
18 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
19 8 a1i ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → 𝑥 ∈ V )
20 9 a1i ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → 𝑦 ∈ V )
21 18 2 3 19 20 joindef ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ( join ‘ 𝐾 ) ↔ { 𝑥 , 𝑦 } ∈ dom ( lub ‘ 𝐾 ) ) )
22 17 21 sylibrd ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ( join ‘ 𝐾 ) ) )
23 6 22 relssdv ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ⊆ dom ( join ‘ 𝐾 ) )
24 4 23 eqssd ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
25 24 ex ⊢ ( 𝐾 ∈ Poset → ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) → dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
26 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
27 simpl ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → 𝐾 ∈ Poset )
28 1 26 27 meetdmss ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → dom ( meet ‘ 𝐾 ) ⊆ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
29 5 a1i ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → Rel ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
30 eleq2 ⊢ ( dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) → ( { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ↔ { 𝑥 , 𝑦 } ∈ 𝒫 ( Base ‘ 𝐾 ) ) )
31 14 30 syl5ibr ⊢ ( dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) )
32 31 adantl ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) )
33 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
34 8 a1i ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → 𝑥 ∈ V )
35 9 a1i ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → 𝑦 ∈ V )
36 33 26 27 34 35 meetdef ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ( meet ‘ 𝐾 ) ↔ { 𝑥 , 𝑦 } ∈ dom ( glb ‘ 𝐾 ) ) )
37 32 36 sylibrd ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ dom ( meet ‘ 𝐾 ) ) )
38 29 37 relssdv ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ⊆ dom ( meet ‘ 𝐾 ) )
39 28 38 eqssd ⊢ ( ( 𝐾 ∈ Poset ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
40 39 ex ⊢ ( 𝐾 ∈ Poset → ( dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) → dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
41 25 40 anim12d ⊢ ( 𝐾 ∈ Poset → ( ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) → ( dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∧ dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
42 41 imdistani ⊢ ( ( 𝐾 ∈ Poset ∧ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) ) → ( 𝐾 ∈ Poset ∧ ( dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∧ dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
43 1 18 33 isclat ⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) ) )
44 1 2 26 islat ⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ( join ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ∧ dom ( meet ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
45 42 43 44 3imtr4i ⊢ ( 𝐾 ∈ CLat → 𝐾 ∈ Lat )