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∈V→O∈Poset↔D∈Poset

Proof

Step Hyp Ref Expression
1 odupos.d ⊢D=ODual⁡O
2 1 odupos ⊢O∈Poset→D∈Poset
3 eqid ⊢ODual⁡D=ODual⁡D
4 3 odupos ⊢D∈Poset→ODual⁡D∈Poset
5 fvexd ⊢O∈V→ODual⁡D∈V
6 id ⊢O∈V→O∈V
7 eqid ⊢BaseO=BaseO
8 1 7 odubas ⊢BaseO=BaseD
9 3 8 odubas ⊢BaseO=BaseODual⁡D
10 9 a1i ⊢O∈V→BaseO=BaseODual⁡D
11 eqidd ⊢O∈V→BaseO=BaseO
12 eqid ⊢≤O=≤O
13 1 12 oduleval ⊢≤O-1=≤D
14 3 13 oduleval ⊢≤O-1-1=≤ODual⁡D
15 14 eqcomi ⊢≤ODual⁡D=≤O-1-1
16 15 breqi ⊢a≤ODual⁡Db↔a≤O-1-1b
17 vex ⊢a∈V
18 vex ⊢b∈V
19 17 18 brcnv ⊢a≤O-1-1b↔b≤O-1a
20 18 17 brcnv ⊢b≤O-1a↔a≤Ob
21 16 19 20 3bitri ⊢a≤ODual⁡Db↔a≤Ob
22 21 a1i ⊢O∈V∧a∈BaseO∧b∈BaseO→a≤ODual⁡Db↔a≤Ob
23 5 6 10 11 22 pospropd ⊢O∈V→ODual⁡D∈Poset↔O∈Poset
24 4 23 imbitrid ⊢O∈V→D∈Poset→O∈Poset
25 2 24 impbid2 ⊢O∈V→O∈Poset↔D∈Poset