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 ⊢ 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 ∈ V → Base O = Base ODual ⁡ D
11 eqidd ⊢ O ∈ V → Base O = Base O
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 ⁡ D b ↔ a ≤ O -1 -1 b
17 vex ⊢ a ∈ V
18 vex ⊢ b ∈ V
19 17 18 brcnv ⊢ a ≤ O -1 -1 b ↔ b ≤ O -1 a
20 18 17 brcnv ⊢ b ≤ O -1 a ↔ a ≤ O b
21 16 19 20 3bitri ⊢ a ≤ ODual ⁡ D b ↔ a ≤ O b
22 21 a1i ⊢ O ∈ V ∧ a ∈ Base O ∧ b ∈ Base O → a ≤ ODual ⁡ D b ↔ a ≤ O b
23 5 6 10 11 22 pospropd ⊢ O ∈ V → ODual ⁡ D ∈ Poset ↔ O ∈ Poset
24 4 23 syl5ib ⊢ O ∈ V → D ∈ Poset → O ∈ Poset
25 2 24 impbid2 ⊢ O ∈ V → O ∈ Poset ↔ D ∈ Poset