Theorem odutos

Description: Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018)

	Ref	Expression
Hypothesis	odutos.d	|- D = ( ODual ` K )
Assertion	odutos	|- ( K e. Toset -> D e. Toset )

Proof

Step	Hyp	Ref	Expression
1		odutos.d	|- D = ( ODual ` K )
2		tospos	|- ( K e. Toset -> K e. Poset )
3	1	odupos	|- ( K e. Poset -> D e. Poset )
4	2 3	syl	|- ( K e. Toset -> D e. Poset )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6		eqid	|- ( le ` K ) = ( le ` K )
7	5 6	tleile	|- ( ( K e. Toset /\ y e. ( Base ` K ) /\ x e. ( Base ` K ) ) -> ( y ( le ` K ) x \/ x ( le ` K ) y ) )
8		vex	|- x e. _V
9		vex	|- y e. _V
10	8 9	brcnv	|- ( x `' ( le ` K ) y <-> y ( le ` K ) x )
11	9 8	brcnv	|- ( y `' ( le ` K ) x <-> x ( le ` K ) y )
12	10 11	orbi12i	|- ( ( x `' ( le ` K ) y \/ y `' ( le ` K ) x ) <-> ( y ( le ` K ) x \/ x ( le ` K ) y ) )
13	7 12	sylibr	|- ( ( K e. Toset /\ y e. ( Base ` K ) /\ x e. ( Base ` K ) ) -> ( x `' ( le ` K ) y \/ y `' ( le ` K ) x ) )
14	13	3com23	|- ( ( K e. Toset /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x `' ( le ` K ) y \/ y `' ( le ` K ) x ) )
15	14	3expb	|- ( ( K e. Toset /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x `' ( le ` K ) y \/ y `' ( le ` K ) x ) )
16	15	ralrimivva	|- ( K e. Toset -> A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( x `' ( le ` K ) y \/ y `' ( le ` K ) x ) )
17	1 5	odubas	|- ( Base ` K ) = ( Base ` D )
18	1 6	oduleval	|- `' ( le ` K ) = ( le ` D )
19	17 18	istos	|- ( D e. Toset <-> ( D e. Poset /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( x `' ( le ` K ) y \/ y `' ( le ` K ) x ) ) )
20	4 16 19	sylanbrc	|- ( K e. Toset -> D e. Toset )