This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid 
 |-  ( O e. V -> ( D e. Poset -> O e. Poset ) )
25 2 24 impbid2 
 |-  ( O e. V -> ( O e. Poset <-> D e. Poset ) )