# Metamath Proof Explorer

## Theorem odutos

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

Ref Expression
Hypothesis odutos.d ${⊢}{D}=\mathrm{ODual}\left({K}\right)$
Assertion odutos ${⊢}{K}\in \mathrm{Toset}\to {D}\in \mathrm{Toset}$

### Proof

Step Hyp Ref Expression
1 odutos.d ${⊢}{D}=\mathrm{ODual}\left({K}\right)$
2 tospos ${⊢}{K}\in \mathrm{Toset}\to {K}\in \mathrm{Poset}$
3 1 odupos ${⊢}{K}\in \mathrm{Poset}\to {D}\in \mathrm{Poset}$
4 2 3 syl ${⊢}{K}\in \mathrm{Toset}\to {D}\in \mathrm{Poset}$
5 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
6 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
7 5 6 tleile ${⊢}\left({K}\in \mathrm{Toset}\wedge {y}\in {\mathrm{Base}}_{{K}}\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to \left({y}{\le }_{{K}}{x}\vee {x}{\le }_{{K}}{y}\right)$
8 vex ${⊢}{x}\in \mathrm{V}$
9 vex ${⊢}{y}\in \mathrm{V}$
10 8 9 brcnv ${⊢}{x}{{\le }_{{K}}}^{-1}{y}↔{y}{\le }_{{K}}{x}$
11 9 8 brcnv ${⊢}{y}{{\le }_{{K}}}^{-1}{x}↔{x}{\le }_{{K}}{y}$
12 10 11 orbi12i ${⊢}\left({x}{{\le }_{{K}}}^{-1}{y}\vee {y}{{\le }_{{K}}}^{-1}{x}\right)↔\left({y}{\le }_{{K}}{x}\vee {x}{\le }_{{K}}{y}\right)$
13 7 12 sylibr ${⊢}\left({K}\in \mathrm{Toset}\wedge {y}\in {\mathrm{Base}}_{{K}}\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to \left({x}{{\le }_{{K}}}^{-1}{y}\vee {y}{{\le }_{{K}}}^{-1}{x}\right)$
14 13 3com23 ${⊢}\left({K}\in \mathrm{Toset}\wedge {x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\to \left({x}{{\le }_{{K}}}^{-1}{y}\vee {y}{{\le }_{{K}}}^{-1}{x}\right)$
15 14 3expb ${⊢}\left({K}\in \mathrm{Toset}\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\right)\to \left({x}{{\le }_{{K}}}^{-1}{y}\vee {y}{{\le }_{{K}}}^{-1}{x}\right)$
16 15 ralrimivva ${⊢}{K}\in \mathrm{Toset}\to \forall {x}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({x}{{\le }_{{K}}}^{-1}{y}\vee {y}{{\le }_{{K}}}^{-1}{x}\right)$
17 1 5 odubas ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{D}}$
18 1 6 oduleval ${⊢}{{\le }_{{K}}}^{-1}={\le }_{{D}}$
19 17 18 istos ${⊢}{D}\in \mathrm{Toset}↔\left({D}\in \mathrm{Poset}\wedge \forall {x}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left({x}{{\le }_{{K}}}^{-1}{y}\vee {y}{{\le }_{{K}}}^{-1}{x}\right)\right)$
20 4 16 19 sylanbrc ${⊢}{K}\in \mathrm{Toset}\to {D}\in \mathrm{Toset}$