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 
|- ( ph -> B = ( Base ` K ) )
isclatd.u 
|- ( ph -> U = ( lub ` K ) )
isclatd.g 
|- ( ph -> G = ( glb ` K ) )
isclatd.k 
|- ( ph -> K e. Poset )
isclatd.1 
|- ( ( ph /\ s C_ B ) -> s e. dom U )
isclatd.2 
|- ( ( ph /\ s C_ B ) -> s e. dom G )
Assertion isclatd 
|- ( ph -> K e. CLat )

Proof

Step Hyp Ref Expression
1 isclatd.b 
 |-  ( ph -> B = ( Base ` K ) )
2 isclatd.u 
 |-  ( ph -> U = ( lub ` K ) )
3 isclatd.g 
 |-  ( ph -> G = ( glb ` K ) )
4 isclatd.k 
 |-  ( ph -> K e. Poset )
5 isclatd.1 
 |-  ( ( ph /\ s C_ B ) -> s e. dom U )
6 isclatd.2 
 |-  ( ( ph /\ s C_ B ) -> s e. dom G )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 eqid 
 |-  ( le ` K ) = ( le ` K )
9 eqid 
 |-  ( lub ` K ) = ( lub ` K )
10 biid 
 |-  ( ( A. y e. t y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. t y ( le ` K ) z -> x ( le ` K ) z ) ) <-> ( A. y e. t y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. t y ( le ` K ) z -> x ( le ` K ) z ) ) )
11 7 8 9 10 4 lubdm 
 |-  ( ph -> dom ( lub ` K ) = { t e. ~P ( Base ` K ) | E! x e. ( Base ` K ) ( A. y e. t y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. t y ( le ` K ) z -> x ( le ` K ) z ) ) } )
12 ssrab2 
 |-  { t e. ~P ( Base ` K ) | E! x e. ( Base ` K ) ( A. y e. t y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. t y ( le ` K ) z -> x ( le ` K ) z ) ) } C_ ~P ( Base ` K )
13 11 12 eqsstrdi 
 |-  ( ph -> dom ( lub ` K ) C_ ~P ( Base ` K ) )
14 elpwi 
 |-  ( s e. ~P B -> s C_ B )
15 14 5 sylan2 
 |-  ( ( ph /\ s e. ~P B ) -> s e. dom U )
16 15 ralrimiva 
 |-  ( ph -> A. s e. ~P B s e. dom U )
17 dfss3 
 |-  ( ~P B C_ dom U <-> A. s e. ~P B s e. dom U )
18 16 17 sylibr 
 |-  ( ph -> ~P B C_ dom U )
19 1 pweqd 
 |-  ( ph -> ~P B = ~P ( Base ` K ) )
20 2 dmeqd 
 |-  ( ph -> dom U = dom ( lub ` K ) )
21 18 19 20 3sstr3d 
 |-  ( ph -> ~P ( Base ` K ) C_ dom ( lub ` K ) )
22 13 21 eqssd 
 |-  ( ph -> dom ( lub ` K ) = ~P ( Base ` K ) )
23 eqid 
 |-  ( glb ` K ) = ( glb ` K )
24 biid 
 |-  ( ( A. y e. t x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. t z ( le ` K ) y -> z ( le ` K ) x ) ) <-> ( A. y e. t x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. t z ( le ` K ) y -> z ( le ` K ) x ) ) )
25 7 8 23 24 4 glbdm 
 |-  ( ph -> dom ( glb ` K ) = { t e. ~P ( Base ` K ) | E! x e. ( Base ` K ) ( A. y e. t x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. t z ( le ` K ) y -> z ( le ` K ) x ) ) } )
26 ssrab2 
 |-  { t e. ~P ( Base ` K ) | E! x e. ( Base ` K ) ( A. y e. t x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. t z ( le ` K ) y -> z ( le ` K ) x ) ) } C_ ~P ( Base ` K )
27 25 26 eqsstrdi 
 |-  ( ph -> dom ( glb ` K ) C_ ~P ( Base ` K ) )
28 14 6 sylan2 
 |-  ( ( ph /\ s e. ~P B ) -> s e. dom G )
29 28 ralrimiva 
 |-  ( ph -> A. s e. ~P B s e. dom G )
30 dfss3 
 |-  ( ~P B C_ dom G <-> A. s e. ~P B s e. dom G )
31 29 30 sylibr 
 |-  ( ph -> ~P B C_ dom G )
32 3 dmeqd 
 |-  ( ph -> dom G = dom ( glb ` K ) )
33 31 19 32 3sstr3d 
 |-  ( ph -> ~P ( Base ` K ) C_ dom ( glb ` K ) )
34 27 33 eqssd 
 |-  ( ph -> dom ( glb ` K ) = ~P ( Base ` K ) )
35 7 9 23 isclat 
 |-  ( K e. CLat <-> ( K e. Poset /\ ( dom ( lub ` K ) = ~P ( Base ` K ) /\ dom ( glb ` K ) = ~P ( Base ` K ) ) ) )
36 35 biimpri 
 |-  ( ( K e. Poset /\ ( dom ( lub ` K ) = ~P ( Base ` K ) /\ dom ( glb ` K ) = ~P ( Base ` K ) ) ) -> K e. CLat )
37 4 22 34 36 syl12anc 
 |-  ( ph -> K e. CLat )