# 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 𝐷 = ( ODual ‘ 𝑂 )
Assertion oduposb ( 𝑂𝑉 → ( 𝑂 ∈ Poset ↔ 𝐷 ∈ Poset ) )

### Proof

Step Hyp Ref Expression
1 odupos.d 𝐷 = ( ODual ‘ 𝑂 )
2 1 odupos ( 𝑂 ∈ Poset → 𝐷 ∈ Poset )
3 eqid ( ODual ‘ 𝐷 ) = ( ODual ‘ 𝐷 )
4 3 odupos ( 𝐷 ∈ Poset → ( ODual ‘ 𝐷 ) ∈ Poset )
5 fvexd ( 𝑂𝑉 → ( ODual ‘ 𝐷 ) ∈ V )
6 id ( 𝑂𝑉𝑂𝑉 )
7 eqid ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
8 1 7 odubas ( Base ‘ 𝑂 ) = ( Base ‘ 𝐷 )
9 3 8 odubas ( Base ‘ 𝑂 ) = ( Base ‘ ( ODual ‘ 𝐷 ) )
10 9 a1i ( 𝑂𝑉 → ( Base ‘ 𝑂 ) = ( Base ‘ ( ODual ‘ 𝐷 ) ) )
11 eqidd ( 𝑂𝑉 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 ) )
12 eqid ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
13 1 12 oduleval ( le ‘ 𝑂 ) = ( le ‘ 𝐷 )
14 3 13 oduleval ( le ‘ 𝑂 ) = ( le ‘ ( ODual ‘ 𝐷 ) )
15 14 eqcomi ( le ‘ ( ODual ‘ 𝐷 ) ) = ( le ‘ 𝑂 )
16 15 breqi ( 𝑎 ( le ‘ ( ODual ‘ 𝐷 ) ) 𝑏𝑎 ( le ‘ 𝑂 ) 𝑏 )
17 vex 𝑎 ∈ V
18 vex 𝑏 ∈ V
19 17 18 brcnv ( 𝑎 ( le ‘ 𝑂 ) 𝑏𝑏 ( le ‘ 𝑂 ) 𝑎 )
20 18 17 brcnv ( 𝑏 ( le ‘ 𝑂 ) 𝑎𝑎 ( le ‘ 𝑂 ) 𝑏 )
21 16 19 20 3bitri ( 𝑎 ( le ‘ ( ODual ‘ 𝐷 ) ) 𝑏𝑎 ( le ‘ 𝑂 ) 𝑏 )
22 21 a1i ( ( 𝑂𝑉 ∧ ( 𝑎 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ) ) → ( 𝑎 ( le ‘ ( ODual ‘ 𝐷 ) ) 𝑏𝑎 ( le ‘ 𝑂 ) 𝑏 ) )
23 5 6 10 11 22 pospropd ( 𝑂𝑉 → ( ( ODual ‘ 𝐷 ) ∈ Poset ↔ 𝑂 ∈ Poset ) )
24 4 23 syl5ib ( 𝑂𝑉 → ( 𝐷 ∈ Poset → 𝑂 ∈ Poset ) )
25 2 24 impbid2 ( 𝑂𝑉 → ( 𝑂 ∈ Poset ↔ 𝐷 ∈ Poset ) )