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 
|- ( K e. CLat -> K e. Lat )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` K ) = ( Base ` K )
2 eqid 
 |-  ( join ` K ) = ( join ` K )
3 simpl 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> K e. Poset )
4 1 2 3 joindmss 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> dom ( join ` K ) C_ ( ( Base ` K ) X. ( Base ` K ) ) )
5 relxp 
 |-  Rel ( ( Base ` K ) X. ( Base ` K ) )
6 5 a1i 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> Rel ( ( Base ` K ) X. ( Base ` K ) ) )
7 opelxp 
 |-  ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) <-> ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) )
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 8 9 prss 
 |-  ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) <-> { x , y } C_ ( Base ` K ) )
11 7 10 sylbb 
 |-  ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> { x , y } C_ ( Base ` K ) )
12 prex 
 |-  { x , y } e. _V
13 12 elpw 
 |-  ( { x , y } e. ~P ( Base ` K ) <-> { x , y } C_ ( Base ` K ) )
14 11 13 sylibr 
 |-  ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> { x , y } e. ~P ( Base ` K ) )
15 eleq2 
 |-  ( dom ( lub ` K ) = ~P ( Base ` K ) -> ( { x , y } e. dom ( lub ` K ) <-> { x , y } e. ~P ( Base ` K ) ) )
16 14 15 syl5ibr 
 |-  ( dom ( lub ` K ) = ~P ( Base ` K ) -> ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> { x , y } e. dom ( lub ` K ) ) )
17 16 adantl 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> { x , y } e. dom ( lub ` K ) ) )
18 eqid 
 |-  ( lub ` K ) = ( lub ` K )
19 8 a1i 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> x e. _V )
20 9 a1i 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> y e. _V )
21 18 2 3 19 20 joindef 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> ( <. x , y >. e. dom ( join ` K ) <-> { x , y } e. dom ( lub ` K ) ) )
22 17 21 sylibrd 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> <. x , y >. e. dom ( join ` K ) ) )
23 6 22 relssdv 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> ( ( Base ` K ) X. ( Base ` K ) ) C_ dom ( join ` K ) )
24 4 23 eqssd 
 |-  ( ( K e. Poset /\ dom ( lub ` K ) = ~P ( Base ` K ) ) -> dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) )
25 24 ex 
 |-  ( K e. Poset -> ( dom ( lub ` K ) = ~P ( Base ` K ) -> dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) )
26 eqid 
 |-  ( meet ` K ) = ( meet ` K )
27 simpl 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> K e. Poset )
28 1 26 27 meetdmss 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> dom ( meet ` K ) C_ ( ( Base ` K ) X. ( Base ` K ) ) )
29 5 a1i 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> Rel ( ( Base ` K ) X. ( Base ` K ) ) )
30 eleq2 
 |-  ( dom ( glb ` K ) = ~P ( Base ` K ) -> ( { x , y } e. dom ( glb ` K ) <-> { x , y } e. ~P ( Base ` K ) ) )
31 14 30 syl5ibr 
 |-  ( dom ( glb ` K ) = ~P ( Base ` K ) -> ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> { x , y } e. dom ( glb ` K ) ) )
32 31 adantl 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> { x , y } e. dom ( glb ` K ) ) )
33 eqid 
 |-  ( glb ` K ) = ( glb ` K )
34 8 a1i 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> x e. _V )
35 9 a1i 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> y e. _V )
36 33 26 27 34 35 meetdef 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> ( <. x , y >. e. dom ( meet ` K ) <-> { x , y } e. dom ( glb ` K ) ) )
37 32 36 sylibrd 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> ( <. x , y >. e. ( ( Base ` K ) X. ( Base ` K ) ) -> <. x , y >. e. dom ( meet ` K ) ) )
38 29 37 relssdv 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> ( ( Base ` K ) X. ( Base ` K ) ) C_ dom ( meet ` K ) )
39 28 38 eqssd 
 |-  ( ( K e. Poset /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) )
40 39 ex 
 |-  ( K e. Poset -> ( dom ( glb ` K ) = ~P ( Base ` K ) -> dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) )
41 25 40 anim12d 
 |-  ( K e. Poset -> ( ( dom ( lub ` K ) = ~P ( Base ` K ) /\ dom ( glb ` K ) = ~P ( Base ` K ) ) -> ( dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) /\ dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
42 41 imdistani 
 |-  ( ( K e. Poset /\ ( dom ( lub ` K ) = ~P ( Base ` K ) /\ dom ( glb ` K ) = ~P ( Base ` K ) ) ) -> ( K e. Poset /\ ( dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) /\ dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
43 1 18 33 isclat 
 |-  ( K e. CLat <-> ( K e. Poset /\ ( dom ( lub ` K ) = ~P ( Base ` K ) /\ dom ( glb ` K ) = ~P ( Base ` K ) ) ) )
44 1 2 26 islat 
 |-  ( K e. Lat <-> ( K e. Poset /\ ( dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) /\ dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
45 42 43 44 3imtr4i 
 |-  ( K e. CLat -> K e. Lat )