# Metamath Proof Explorer

## Theorem oduposb

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 oduposb
`|- ( O e. V -> ( O e. Poset <-> D e. Poset ) )`

### Proof

Step Hyp Ref Expression
1 odupos.d
` |-  D = ( ODual ` O )`
2 1 odupos
` |-  ( O e. Poset -> D e. Poset )`
3 eqid
` |-  ( ODual ` D ) = ( ODual ` D )`
4 3 odupos
` |-  ( D e. Poset -> ( ODual ` D ) e. Poset )`
5 fvexd
` |-  ( O e. V -> ( ODual ` D ) e. _V )`
6 id
` |-  ( O e. V -> O e. V )`
7 eqid
` |-  ( Base ` O ) = ( Base ` O )`
8 1 7 odubas
` |-  ( Base ` O ) = ( Base ` D )`
9 3 8 odubas
` |-  ( Base ` O ) = ( Base ` ( ODual ` D ) )`
10 9 a1i
` |-  ( O e. V -> ( Base ` O ) = ( Base ` ( ODual ` D ) ) )`
11 eqidd
` |-  ( O e. V -> ( Base ` O ) = ( Base ` O ) )`
12 eqid
` |-  ( le ` O ) = ( le ` O )`
13 1 12 oduleval
` |-  `' ( le ` O ) = ( le ` D )`
14 3 13 oduleval
` |-  `' `' ( le ` O ) = ( le ` ( ODual ` D ) )`
15 14 eqcomi
` |-  ( le ` ( ODual ` D ) ) = `' `' ( le ` O )`
16 15 breqi
` |-  ( a ( le ` ( ODual ` D ) ) b <-> a `' `' ( le ` O ) b )`
17 vex
` |-  a e. _V`
18 vex
` |-  b e. _V`
19 17 18 brcnv
` |-  ( a `' `' ( le ` O ) b <-> b `' ( le ` O ) a )`
20 18 17 brcnv
` |-  ( b `' ( le ` O ) a <-> a ( le ` O ) b )`
21 16 19 20 3bitri
` |-  ( a ( le ` ( ODual ` D ) ) b <-> a ( le ` O ) b )`
22 21 a1i
` |-  ( ( O e. V /\ ( a e. ( Base ` O ) /\ b e. ( Base ` O ) ) ) -> ( a ( le ` ( ODual ` D ) ) b <-> a ( le ` O ) b ) )`
23 5 6 10 11 22 pospropd
` |-  ( O e. V -> ( ( ODual ` D ) e. Poset <-> O e. Poset ) )`
24 4 23 syl5ib
` |-  ( O e. V -> ( D e. Poset -> O e. Poset ) )`
25 2 24 impbid2
` |-  ( O e. V -> ( O e. Poset <-> D e. Poset ) )`