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 ) )