Metamath Proof Explorer

Theorem oduclatb

Description: Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypothesis oduglb.d 
|- D = ( ODual ` O )
Assertion oduclatb 
|- ( O e. CLat <-> D e. CLat )

Proof

Step Hyp Ref Expression
1 oduglb.d 
 |-  D = ( ODual ` O )
2 elex 
 |-  ( O e. CLat -> O e. _V )
3 noel 
 |-  -. ( ( lub ` (/) ) ` (/) ) e. (/)
4 ssid 
 |-  (/) C_ (/)
5 base0 
 |-  (/) = ( Base ` (/) )
6 eqid 
 |-  ( lub ` (/) ) = ( lub ` (/) )
7 5 6 clatlubcl 
 |-  ( ( (/) e. CLat /\ (/) C_ (/) ) -> ( ( lub ` (/) ) ` (/) ) e. (/) )
8 4 7 mpan2 
 |-  ( (/) e. CLat -> ( ( lub ` (/) ) ` (/) ) e. (/) )
9 3 8 mto 
 |-  -. (/) e. CLat
10 fvprc 
 |-  ( -. O e. _V -> ( ODual ` O ) = (/) )
11 1 10 syl5eq 
 |-  ( -. O e. _V -> D = (/) )
12 11 eleq1d 
 |-  ( -. O e. _V -> ( D e. CLat <-> (/) e. CLat ) )
13 9 12 mtbiri 
 |-  ( -. O e. _V -> -. D e. CLat )
14 13 con4i 
 |-  ( D e. CLat -> O e. _V )
15 1 oduposb 
 |-  ( O e. _V -> ( O e. Poset <-> D e. Poset ) )
16 ancom 
 |-  ( ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) <-> ( dom ( glb ` O ) = ~P ( Base ` O ) /\ dom ( lub ` O ) = ~P ( Base ` O ) ) )
17 eqid 
 |-  ( glb ` O ) = ( glb ` O )
18 1 17 odulub 
 |-  ( O e. _V -> ( glb ` O ) = ( lub ` D ) )
19 18 dmeqd 
 |-  ( O e. _V -> dom ( glb ` O ) = dom ( lub ` D ) )
20 19 eqeq1d 
 |-  ( O e. _V -> ( dom ( glb ` O ) = ~P ( Base ` O ) <-> dom ( lub ` D ) = ~P ( Base ` O ) ) )
21 eqid 
 |-  ( lub ` O ) = ( lub ` O )
22 1 21 oduglb 
 |-  ( O e. _V -> ( lub ` O ) = ( glb ` D ) )
23 22 dmeqd 
 |-  ( O e. _V -> dom ( lub ` O ) = dom ( glb ` D ) )
24 23 eqeq1d 
 |-  ( O e. _V -> ( dom ( lub ` O ) = ~P ( Base ` O ) <-> dom ( glb ` D ) = ~P ( Base ` O ) ) )
25 20 24 anbi12d 
 |-  ( O e. _V -> ( ( dom ( glb ` O ) = ~P ( Base ` O ) /\ dom ( lub ` O ) = ~P ( Base ` O ) ) <-> ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) )
26 16 25 syl5bb 
 |-  ( O e. _V -> ( ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) <-> ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) )
27 15 26 anbi12d 
 |-  ( O e. _V -> ( ( O e. Poset /\ ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) ) <-> ( D e. Poset /\ ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) ) )
28 eqid 
 |-  ( Base ` O ) = ( Base ` O )
29 28 21 17 isclat 
 |-  ( O e. CLat <-> ( O e. Poset /\ ( dom ( lub ` O ) = ~P ( Base ` O ) /\ dom ( glb ` O ) = ~P ( Base ` O ) ) ) )
30 1 28 odubas 
 |-  ( Base ` O ) = ( Base ` D )
31 eqid 
 |-  ( lub ` D ) = ( lub ` D )
32 eqid 
 |-  ( glb ` D ) = ( glb ` D )
33 30 31 32 isclat 
 |-  ( D e. CLat <-> ( D e. Poset /\ ( dom ( lub ` D ) = ~P ( Base ` O ) /\ dom ( glb ` D ) = ~P ( Base ` O ) ) ) )
34 27 29 33 3bitr4g 
 |-  ( O e. _V -> ( O e. CLat <-> D e. CLat ) )
35 2 14 34 pm5.21nii 
 |-  ( O e. CLat <-> D e. CLat )