This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isclatd

Description: The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Hypotheses isclatd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
isclatd.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
isclatd.g ⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐾 ) )
isclatd.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
isclatd.1 ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝑈 )
isclatd.2 ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝐺 )
Assertion isclatd ( 𝜑 → 𝐾 ∈ CLat )

Proof

Step Hyp Ref Expression
1 isclatd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 isclatd.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
3 isclatd.g ⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐾 ) )
4 isclatd.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 isclatd.1 ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝑈 )
6 isclatd.2 ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝐺 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
10 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
11 7 8 9 10 4 lubdm ⊢ ( 𝜑 → dom ( lub ‘ 𝐾 ) = { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) } )
12 ssrab2 ⊢ { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) } ⊆ 𝒫 ( Base ‘ 𝐾 )
13 11 12 eqsstrdi ⊢ ( 𝜑 → dom ( lub ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) )
14 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵 )
15 14 5 sylan2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ dom 𝑈 )
16 15 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝑈 )
17 dfss3 ⊢ ( 𝒫 𝐵 ⊆ dom 𝑈 ↔ ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝑈 )
18 16 17 sylibr ⊢ ( 𝜑 → 𝒫 𝐵 ⊆ dom 𝑈 )
19 1 pweqd ⊢ ( 𝜑 → 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐾 ) )
20 2 dmeqd ⊢ ( 𝜑 → dom 𝑈 = dom ( lub ‘ 𝐾 ) )
21 18 19 20 3sstr3d ⊢ ( 𝜑 → 𝒫 ( Base ‘ 𝐾 ) ⊆ dom ( lub ‘ 𝐾 ) )
22 13 21 eqssd ⊢ ( 𝜑 → dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) )
23 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
24 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
25 7 8 23 24 4 glbdm ⊢ ( 𝜑 → dom ( glb ‘ 𝐾 ) = { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } )
26 ssrab2 ⊢ { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } ⊆ 𝒫 ( Base ‘ 𝐾 )
27 25 26 eqsstrdi ⊢ ( 𝜑 → dom ( glb ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) )
28 14 6 sylan2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ dom 𝐺 )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝐺 )
30 dfss3 ⊢ ( 𝒫 𝐵 ⊆ dom 𝐺 ↔ ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝐺 )
31 29 30 sylibr ⊢ ( 𝜑 → 𝒫 𝐵 ⊆ dom 𝐺 )
32 3 dmeqd ⊢ ( 𝜑 → dom 𝐺 = dom ( glb ‘ 𝐾 ) )
33 31 19 32 3sstr3d ⊢ ( 𝜑 → 𝒫 ( Base ‘ 𝐾 ) ⊆ dom ( glb ‘ 𝐾 ) )
34 27 33 eqssd ⊢ ( 𝜑 → dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) )
35 7 9 23 isclat ⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) ) )
36 35 biimpri ⊢ ( ( 𝐾 ∈ Poset ∧ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) ) → 𝐾 ∈ CLat )
37 4 22 34 36 syl12anc ⊢ ( 𝜑 → 𝐾 ∈ CLat )