# 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 syl5bi
` |-  ( ( 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 )`