Theorem oduposb

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	oduposb	|- ( O e. V -> ( O e. Poset <-> D e. Poset ) )

Proof

Step	Hyp	Ref	Expression
1		odupos.d	|- D = ( ODual ` O )
2	1	odupos	|- ( O e. Poset -> D e. Poset )
3		eqid	|- ( ODual ` D ) = ( ODual ` D )
4	3	odupos	|- ( D e. Poset -> ( ODual ` D ) e. Poset )
5		fvexd	|- ( O e. V -> ( ODual ` D ) e. _V )
6		id	|- ( O e. V -> O e. V )
7		eqid	|- ( Base ` O ) = ( Base ` O )
8	1 7	odubas	|- ( Base ` O ) = ( Base ` D )
9	3 8	odubas	|- ( Base ` O ) = ( Base ` ( ODual ` D ) )
10	9	a1i	|- ( O e. V -> ( Base ` O ) = ( Base ` ( ODual ` D ) ) )
11		eqidd	|- ( O e. V -> ( Base ` O ) = ( Base ` O ) )
12		eqid	|- ( le ` O ) = ( le ` O )
13	1 12	oduleval	|- `' ( le ` O ) = ( le ` D )
14	3 13	oduleval	|- `' `' ( le ` O ) = ( le ` ( ODual ` D ) )
15	14	eqcomi	|- ( le ` ( ODual ` D ) ) = `' `' ( le ` O )
16	15	breqi	|- ( a ( le ` ( ODual ` D ) ) b <-> a `' `' ( le ` O ) b )
17		vex	|- a e. _V
18		vex	|- b e. _V
19	17 18	brcnv	|- ( a `' `' ( le ` O ) b <-> b `' ( le ` O ) a )
20	18 17	brcnv	|- ( b `' ( le ` O ) a <-> a ( le ` O ) b )
21	16 19 20	3bitri	|- ( a ( le ` ( ODual ` D ) ) b <-> a ( le ` O ) b )
22	21	a1i	|- ( ( O e. V /\ ( a e. ( Base ` O ) /\ b e. ( Base ` O ) ) ) -> ( a ( le ` ( ODual ` D ) ) b <-> a ( le ` O ) b ) )
23	5 6 10 11 22	pospropd	|- ( O e. V -> ( ( ODual ` D ) e. Poset <-> O e. Poset ) )
24	4 23	syl5ib	|- ( O e. V -> ( D e. Poset -> O e. Poset ) )
25	2 24	impbid2	|- ( O e. V -> ( O e. Poset <-> D e. Poset ) )