# 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}=\mathrm{ODual}\left({O}\right)$
Assertion oduposb ${⊢}{O}\in {V}\to \left({O}\in \mathrm{Poset}↔{D}\in \mathrm{Poset}\right)$

### Proof

Step Hyp Ref Expression
1 odupos.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 1 odupos ${⊢}{O}\in \mathrm{Poset}\to {D}\in \mathrm{Poset}$
3 eqid ${⊢}\mathrm{ODual}\left({D}\right)=\mathrm{ODual}\left({D}\right)$
4 3 odupos ${⊢}{D}\in \mathrm{Poset}\to \mathrm{ODual}\left({D}\right)\in \mathrm{Poset}$
5 fvexd ${⊢}{O}\in {V}\to \mathrm{ODual}\left({D}\right)\in \mathrm{V}$
6 id ${⊢}{O}\in {V}\to {O}\in {V}$
7 eqid ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{O}}$
8 1 7 odubas ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{D}}$
9 3 8 odubas ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{\mathrm{ODual}\left({D}\right)}$
10 9 a1i ${⊢}{O}\in {V}\to {\mathrm{Base}}_{{O}}={\mathrm{Base}}_{\mathrm{ODual}\left({D}\right)}$
11 eqidd ${⊢}{O}\in {V}\to {\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{O}}$
12 eqid ${⊢}{\le }_{{O}}={\le }_{{O}}$
13 1 12 oduleval ${⊢}{{\le }_{{O}}}^{-1}={\le }_{{D}}$
14 3 13 oduleval ${⊢}{{{\le }_{{O}}}^{-1}}^{-1}={\le }_{\mathrm{ODual}\left({D}\right)}$
15 14 eqcomi ${⊢}{\le }_{\mathrm{ODual}\left({D}\right)}={{{\le }_{{O}}}^{-1}}^{-1}$
16 15 breqi ${⊢}{a}{\le }_{\mathrm{ODual}\left({D}\right)}{b}↔{a}{{{\le }_{{O}}}^{-1}}^{-1}{b}$
17 vex ${⊢}{a}\in \mathrm{V}$
18 vex ${⊢}{b}\in \mathrm{V}$
19 17 18 brcnv ${⊢}{a}{{{\le }_{{O}}}^{-1}}^{-1}{b}↔{b}{{\le }_{{O}}}^{-1}{a}$
20 18 17 brcnv ${⊢}{b}{{\le }_{{O}}}^{-1}{a}↔{a}{\le }_{{O}}{b}$
21 16 19 20 3bitri ${⊢}{a}{\le }_{\mathrm{ODual}\left({D}\right)}{b}↔{a}{\le }_{{O}}{b}$
22 21 a1i ${⊢}\left({O}\in {V}\wedge \left({a}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\right)\right)\to \left({a}{\le }_{\mathrm{ODual}\left({D}\right)}{b}↔{a}{\le }_{{O}}{b}\right)$
23 5 6 10 11 22 pospropd ${⊢}{O}\in {V}\to \left(\mathrm{ODual}\left({D}\right)\in \mathrm{Poset}↔{O}\in \mathrm{Poset}\right)$
24 4 23 syl5ib ${⊢}{O}\in {V}\to \left({D}\in \mathrm{Poset}\to {O}\in \mathrm{Poset}\right)$
25 2 24 impbid2 ${⊢}{O}\in {V}\to \left({O}\in \mathrm{Poset}↔{D}\in \mathrm{Poset}\right)$