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

Proof

Step Hyp Ref Expression
1 odupos.d ⊢D=ODual⁡O
2 1 fvexi ⊢D∈V
3 2 a1i ⊢O∈Poset→D∈V
4 eqid ⊢BaseO=BaseO
5 1 4 odubas ⊢BaseO=BaseD
6 5 a1i ⊢O∈Poset→BaseO=BaseD
7 eqid ⊢≤O=≤O
8 1 7 oduleval ⊢≤O-1=≤D
9 8 a1i ⊢O∈Poset→≤O-1=≤D
10 4 7 posref ⊢O∈Poset∧a∈BaseO→a≤Oa
11 vex ⊢a∈V
12 11 11 brcnv ⊢a≤O-1a↔a≤Oa
13 10 12 sylibr ⊢O∈Poset∧a∈BaseO→a≤O-1a
14 vex ⊢b∈V
15 11 14 brcnv ⊢a≤O-1b↔b≤Oa
16 14 11 brcnv ⊢b≤O-1a↔a≤Ob
17 15 16 anbi12ci ⊢a≤O-1b∧b≤O-1a↔a≤Ob∧b≤Oa
18 4 7 posasymb ⊢O∈Poset∧a∈BaseO∧b∈BaseO→a≤Ob∧b≤Oa↔a=b
19 18 biimpd ⊢O∈Poset∧a∈BaseO∧b∈BaseO→a≤Ob∧b≤Oa→a=b
20 17 19 biimtrid ⊢O∈Poset∧a∈BaseO∧b∈BaseO→a≤O-1b∧b≤O-1a→a=b
21 3anrev ⊢a∈BaseO∧b∈BaseO∧c∈BaseO↔c∈BaseO∧b∈BaseO∧a∈BaseO
22 4 7 postr ⊢O∈Poset∧c∈BaseO∧b∈BaseO∧a∈BaseO→c≤Ob∧b≤Oa→c≤Oa
23 21 22 sylan2b ⊢O∈Poset∧a∈BaseO∧b∈BaseO∧c∈BaseO→c≤Ob∧b≤Oa→c≤Oa
24 vex ⊢c∈V
25 14 24 brcnv ⊢b≤O-1c↔c≤Ob
26 15 25 anbi12ci ⊢a≤O-1b∧b≤O-1c↔c≤Ob∧b≤Oa
27 11 24 brcnv ⊢a≤O-1c↔c≤Oa
28 23 26 27 3imtr4g ⊢O∈Poset∧a∈BaseO∧b∈BaseO∧c∈BaseO→a≤O-1b∧b≤O-1c→a≤O-1c
29 3 6 9 13 20 28 isposd ⊢O∈Poset→D∈Poset