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 ⊢ 𝐷 = ( ODual ‘ 𝑂 )
Assertion odupos ( 𝑂 ∈ Poset → 𝐷 ∈ Poset )

Proof

Step Hyp Ref Expression
1 odupos.d ⊢ 𝐷 = ( ODual ‘ 𝑂 )
2 1 fvexi ⊢ 𝐷 ∈ V
3 2 a1i ⊢ ( 𝑂 ∈ Poset → 𝐷 ∈ V )
4 eqid ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
5 1 4 odubas ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝐷 )
6 5 a1i ⊢ ( 𝑂 ∈ Poset → ( Base ‘ 𝑂 ) = ( Base ‘ 𝐷 ) )
7 eqid ⊢ ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
8 1 7 oduleval ⊢ ◡ ( le ‘ 𝑂 ) = ( le ‘ 𝐷 )
9 8 a1i ⊢ ( 𝑂 ∈ Poset → ◡ ( le ‘ 𝑂 ) = ( le ‘ 𝐷 ) )
10 4 7 posref ⊢ ( ( 𝑂 ∈ Poset ∧ 𝑎 ∈ ( Base ‘ 𝑂 ) ) → 𝑎 ( le ‘ 𝑂 ) 𝑎 )
11 vex ⊢ 𝑎 ∈ V
12 11 11 brcnv ⊢ ( 𝑎 ◡ ( le ‘ 𝑂 ) 𝑎 ↔ 𝑎 ( le ‘ 𝑂 ) 𝑎 )
13 10 12 sylibr ⊢ ( ( 𝑂 ∈ Poset ∧ 𝑎 ∈ ( Base ‘ 𝑂 ) ) → 𝑎 ◡ ( le ‘ 𝑂 ) 𝑎 )
14 vex ⊢ 𝑏 ∈ V
15 11 14 brcnv ⊢ ( 𝑎 ◡ ( le ‘ 𝑂 ) 𝑏 ↔ 𝑏 ( le ‘ 𝑂 ) 𝑎 )
16 14 11 brcnv ⊢ ( 𝑏 ◡ ( le ‘ 𝑂 ) 𝑎 ↔ 𝑎 ( le ‘ 𝑂 ) 𝑏 )
17 15 16 anbi12ci ⊢ ( ( 𝑎 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ◡ ( le ‘ 𝑂 ) 𝑎 ) ↔ ( 𝑎 ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ( le ‘ 𝑂 ) 𝑎 ) )
18 4 7 posasymb ⊢ ( ( 𝑂 ∈ Poset ∧ 𝑎 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ) → ( ( 𝑎 ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ( le ‘ 𝑂 ) 𝑎 ) ↔ 𝑎 = 𝑏 ) )
19 18 biimpd ⊢ ( ( 𝑂 ∈ Poset ∧ 𝑎 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ) → ( ( 𝑎 ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ( le ‘ 𝑂 ) 𝑎 ) → 𝑎 = 𝑏 ) )
20 17 19 syl5bi ⊢ ( ( 𝑂 ∈ Poset ∧ 𝑎 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ) → ( ( 𝑎 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ◡ ( le ‘ 𝑂 ) 𝑎 ) → 𝑎 = 𝑏 ) )
21 3anrev ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ∧ 𝑐 ∈ ( Base ‘ 𝑂 ) ) ↔ ( 𝑐 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ∧ 𝑎 ∈ ( Base ‘ 𝑂 ) ) )
22 4 7 postr ⊢ ( ( 𝑂 ∈ Poset ∧ ( 𝑐 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ∧ 𝑎 ∈ ( Base ‘ 𝑂 ) ) ) → ( ( 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ( le ‘ 𝑂 ) 𝑎 ) → 𝑐 ( le ‘ 𝑂 ) 𝑎 ) )
23 21 22 sylan2b ⊢ ( ( 𝑂 ∈ Poset ∧ ( 𝑎 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ∧ 𝑐 ∈ ( Base ‘ 𝑂 ) ) ) → ( ( 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ( le ‘ 𝑂 ) 𝑎 ) → 𝑐 ( le ‘ 𝑂 ) 𝑎 ) )
24 vex ⊢ 𝑐 ∈ V
25 14 24 brcnv ⊢ ( 𝑏 ◡ ( le ‘ 𝑂 ) 𝑐 ↔ 𝑐 ( le ‘ 𝑂 ) 𝑏 )
26 15 25 anbi12ci ⊢ ( ( 𝑎 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ◡ ( le ‘ 𝑂 ) 𝑐 ) ↔ ( 𝑐 ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ( le ‘ 𝑂 ) 𝑎 ) )
27 11 24 brcnv ⊢ ( 𝑎 ◡ ( le ‘ 𝑂 ) 𝑐 ↔ 𝑐 ( le ‘ 𝑂 ) 𝑎 )
28 23 26 27 3imtr4g ⊢ ( ( 𝑂 ∈ Poset ∧ ( 𝑎 ∈ ( Base ‘ 𝑂 ) ∧ 𝑏 ∈ ( Base ‘ 𝑂 ) ∧ 𝑐 ∈ ( Base ‘ 𝑂 ) ) ) → ( ( 𝑎 ◡ ( le ‘ 𝑂 ) 𝑏 ∧ 𝑏 ◡ ( le ‘ 𝑂 ) 𝑐 ) → 𝑎 ◡ ( le ‘ 𝑂 ) 𝑐 ) )
29 3 6 9 13 20 28 isposd ⊢ ( 𝑂 ∈ Poset → 𝐷 ∈ Poset )