Metamath Proof Explorer

Theorem odupos

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

Ref Expression
Hypothesis odupos.d 
|- D = ( ODual ` O )
Assertion odupos 
|- ( O e. Poset -> D e. Poset )

Proof

Step Hyp Ref Expression
1 odupos.d 
 |-  D = ( ODual ` O )
2 1 fvexi 
 |-  D e. _V
3 2 a1i 
 |-  ( O e. Poset -> D e. _V )
4 eqid 
 |-  ( Base ` O ) = ( Base ` O )
5 1 4 odubas 
 |-  ( Base ` O ) = ( Base ` D )
6 5 a1i 
 |-  ( O e. Poset -> ( Base ` O ) = ( Base ` D ) )
7 eqid 
 |-  ( le ` O ) = ( le ` O )
8 1 7 oduleval 
 |-  `' ( le ` O ) = ( le ` D )
9 8 a1i 
 |-  ( O e. Poset -> `' ( le ` O ) = ( le ` D ) )
10 4 7 posref 
 |-  ( ( O e. Poset /\ a e. ( Base ` O ) ) -> a ( le ` O ) a )
11 vex 
 |-  a e. _V
12 11 11 brcnv 
 |-  ( a `' ( le ` O ) a <-> a ( le ` O ) a )
13 10 12 sylibr 
 |-  ( ( O e. Poset /\ a e. ( Base ` O ) ) -> a `' ( le ` O ) a )
14 vex 
 |-  b e. _V
15 11 14 brcnv 
 |-  ( a `' ( le ` O ) b <-> b ( le ` O ) a )
16 14 11 brcnv 
 |-  ( b `' ( le ` O ) a <-> a ( le ` O ) b )
17 15 16 anbi12ci 
 |-  ( ( a `' ( le ` O ) b /\ b `' ( le ` O ) a ) <-> ( a ( le ` O ) b /\ b ( le ` O ) a ) )
18 4 7 posasymb 
 |-  ( ( O e. Poset /\ a e. ( Base ` O ) /\ b e. ( Base ` O ) ) -> ( ( a ( le ` O ) b /\ b ( le ` O ) a ) <-> a = b ) )
19 18 biimpd 
 |-  ( ( O e. Poset /\ a e. ( Base ` O ) /\ b e. ( Base ` O ) ) -> ( ( a ( le ` O ) b /\ b ( le ` O ) a ) -> a = b ) )
20 17 19 biimtrid 
 |-  ( ( O e. Poset /\ a e. ( Base ` O ) /\ b e. ( Base ` O ) ) -> ( ( a `' ( le ` O ) b /\ b `' ( le ` O ) a ) -> a = b ) )
21 3anrev 
 |-  ( ( a e. ( Base ` O ) /\ b e. ( Base ` O ) /\ c e. ( Base ` O ) ) <-> ( c e. ( Base ` O ) /\ b e. ( Base ` O ) /\ a e. ( Base ` O ) ) )
22 4 7 postr 
 |-  ( ( O e. Poset /\ ( c e. ( Base ` O ) /\ b e. ( Base ` O ) /\ a e. ( Base ` O ) ) ) -> ( ( c ( le ` O ) b /\ b ( le ` O ) a ) -> c ( le ` O ) a ) )
23 21 22 sylan2b 
 |-  ( ( O e. Poset /\ ( a e. ( Base ` O ) /\ b e. ( Base ` O ) /\ c e. ( Base ` O ) ) ) -> ( ( c ( le ` O ) b /\ b ( le ` O ) a ) -> c ( le ` O ) a ) )
24 vex 
 |-  c e. _V
25 14 24 brcnv 
 |-  ( b `' ( le ` O ) c <-> c ( le ` O ) b )
26 15 25 anbi12ci 
 |-  ( ( a `' ( le ` O ) b /\ b `' ( le ` O ) c ) <-> ( c ( le ` O ) b /\ b ( le ` O ) a ) )
27 11 24 brcnv 
 |-  ( a `' ( le ` O ) c <-> c ( le ` O ) a )
28 23 26 27 3imtr4g 
 |-  ( ( O e. Poset /\ ( a e. ( Base ` O ) /\ b e. ( Base ` O ) /\ c e. ( Base ` O ) ) ) -> ( ( a `' ( le ` O ) b /\ b `' ( le ` O ) c ) -> a `' ( le ` O ) c ) )
29 3 6 9 13 20 28 isposd 
 |-  ( O e. Poset -> D e. Poset )