This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( 𝑂 ∈ 𝑉 → ( 𝐷 ∈ Poset → 𝑂 ∈ Poset ) )
25 2 24 impbid2 ⊢ ( 𝑂 ∈ 𝑉 → ( 𝑂 ∈ Poset ↔ 𝐷 ∈ Poset ) )