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 ⊢ Base O = Base O
5 1 4 odubas ⊢ Base O = Base D
6 5 a1i ⊢ O ∈ Poset → Base O = Base D
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 ∈ Base O → a ≤ O a
11 vex ⊢ a ∈ V
12 11 11 brcnv ⊢ a ≤ O -1 a ↔ a ≤ O a
13 10 12 sylibr ⊢ O ∈ Poset ∧ a ∈ Base O → a ≤ O -1 a
14 vex ⊢ b ∈ V
15 11 14 brcnv ⊢ a ≤ O -1 b ↔ b ≤ O a
16 14 11 brcnv ⊢ b ≤ O -1 a ↔ a ≤ O b
17 15 16 anbi12ci ⊢ a ≤ O -1 b ∧ b ≤ O -1 a ↔ a ≤ O b ∧ b ≤ O a
18 4 7 posasymb ⊢ O ∈ Poset ∧ a ∈ Base O ∧ b ∈ Base O → a ≤ O b ∧ b ≤ O a ↔ a = b
19 18 biimpd ⊢ O ∈ Poset ∧ a ∈ Base O ∧ b ∈ Base O → a ≤ O b ∧ b ≤ O a → a = b
20 17 19 syl5bi ⊢ O ∈ Poset ∧ a ∈ Base O ∧ b ∈ Base O → a ≤ O -1 b ∧ b ≤ O -1 a → a = b
21 3anrev ⊢ a ∈ Base O ∧ b ∈ Base O ∧ c ∈ Base O ↔ c ∈ Base O ∧ b ∈ Base O ∧ a ∈ Base O
22 4 7 postr ⊢ O ∈ Poset ∧ c ∈ Base O ∧ b ∈ Base O ∧ a ∈ Base O → c ≤ O b ∧ b ≤ O a → c ≤ O a
23 21 22 sylan2b ⊢ O ∈ Poset ∧ a ∈ Base O ∧ b ∈ Base O ∧ c ∈ Base O → c ≤ O b ∧ b ≤ O a → c ≤ O a
24 vex ⊢ c ∈ V
25 14 24 brcnv ⊢ b ≤ O -1 c ↔ c ≤ O b
26 15 25 anbi12ci ⊢ a ≤ O -1 b ∧ b ≤ O -1 c ↔ c ≤ O b ∧ b ≤ O a
27 11 24 brcnv ⊢ a ≤ O -1 c ↔ c ≤ O a
28 23 26 27 3imtr4g ⊢ O ∈ Poset ∧ a ∈ Base O ∧ b ∈ Base O ∧ c ∈ Base O → a ≤ O -1 b ∧ b ≤ O -1 c → a ≤ O -1 c
29 3 6 9 13 20 28 isposd ⊢ O ∈ Poset → D ∈ Poset