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 ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
Assertion odupos ${⊢}{O}\in \mathrm{Poset}\to {D}\in \mathrm{Poset}$

Proof

Step Hyp Ref Expression
1 odupos.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 1 fvexi ${⊢}{D}\in \mathrm{V}$
3 2 a1i ${⊢}{O}\in \mathrm{Poset}\to {D}\in \mathrm{V}$
4 eqid ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{O}}$
5 1 4 odubas ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{D}}$
6 5 a1i ${⊢}{O}\in \mathrm{Poset}\to {\mathrm{Base}}_{{O}}={\mathrm{Base}}_{{D}}$
7 eqid ${⊢}{\le }_{{O}}={\le }_{{O}}$
8 1 7 oduleval ${⊢}{{\le }_{{O}}}^{-1}={\le }_{{D}}$
9 8 a1i ${⊢}{O}\in \mathrm{Poset}\to {{\le }_{{O}}}^{-1}={\le }_{{D}}$
10 4 7 posref ${⊢}\left({O}\in \mathrm{Poset}\wedge {a}\in {\mathrm{Base}}_{{O}}\right)\to {a}{\le }_{{O}}{a}$
11 vex ${⊢}{a}\in \mathrm{V}$
12 11 11 brcnv ${⊢}{a}{{\le }_{{O}}}^{-1}{a}↔{a}{\le }_{{O}}{a}$
13 10 12 sylibr ${⊢}\left({O}\in \mathrm{Poset}\wedge {a}\in {\mathrm{Base}}_{{O}}\right)\to {a}{{\le }_{{O}}}^{-1}{a}$
14 vex ${⊢}{b}\in \mathrm{V}$
15 11 14 brcnv ${⊢}{a}{{\le }_{{O}}}^{-1}{b}↔{b}{\le }_{{O}}{a}$
16 14 11 brcnv ${⊢}{b}{{\le }_{{O}}}^{-1}{a}↔{a}{\le }_{{O}}{b}$
17 15 16 anbi12ci ${⊢}\left({a}{{\le }_{{O}}}^{-1}{b}\wedge {b}{{\le }_{{O}}}^{-1}{a}\right)↔\left({a}{\le }_{{O}}{b}\wedge {b}{\le }_{{O}}{a}\right)$
18 4 7 posasymb ${⊢}\left({O}\in \mathrm{Poset}\wedge {a}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\right)\to \left(\left({a}{\le }_{{O}}{b}\wedge {b}{\le }_{{O}}{a}\right)↔{a}={b}\right)$
19 18 biimpd ${⊢}\left({O}\in \mathrm{Poset}\wedge {a}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\right)\to \left(\left({a}{\le }_{{O}}{b}\wedge {b}{\le }_{{O}}{a}\right)\to {a}={b}\right)$
20 17 19 syl5bi ${⊢}\left({O}\in \mathrm{Poset}\wedge {a}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\right)\to \left(\left({a}{{\le }_{{O}}}^{-1}{b}\wedge {b}{{\le }_{{O}}}^{-1}{a}\right)\to {a}={b}\right)$
21 3anrev ${⊢}\left({a}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\wedge {c}\in {\mathrm{Base}}_{{O}}\right)↔\left({c}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\wedge {a}\in {\mathrm{Base}}_{{O}}\right)$
22 4 7 postr ${⊢}\left({O}\in \mathrm{Poset}\wedge \left({c}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\wedge {a}\in {\mathrm{Base}}_{{O}}\right)\right)\to \left(\left({c}{\le }_{{O}}{b}\wedge {b}{\le }_{{O}}{a}\right)\to {c}{\le }_{{O}}{a}\right)$
23 21 22 sylan2b ${⊢}\left({O}\in \mathrm{Poset}\wedge \left({a}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\wedge {c}\in {\mathrm{Base}}_{{O}}\right)\right)\to \left(\left({c}{\le }_{{O}}{b}\wedge {b}{\le }_{{O}}{a}\right)\to {c}{\le }_{{O}}{a}\right)$
24 vex ${⊢}{c}\in \mathrm{V}$
25 14 24 brcnv ${⊢}{b}{{\le }_{{O}}}^{-1}{c}↔{c}{\le }_{{O}}{b}$
26 15 25 anbi12ci ${⊢}\left({a}{{\le }_{{O}}}^{-1}{b}\wedge {b}{{\le }_{{O}}}^{-1}{c}\right)↔\left({c}{\le }_{{O}}{b}\wedge {b}{\le }_{{O}}{a}\right)$
27 11 24 brcnv ${⊢}{a}{{\le }_{{O}}}^{-1}{c}↔{c}{\le }_{{O}}{a}$
28 23 26 27 3imtr4g ${⊢}\left({O}\in \mathrm{Poset}\wedge \left({a}\in {\mathrm{Base}}_{{O}}\wedge {b}\in {\mathrm{Base}}_{{O}}\wedge {c}\in {\mathrm{Base}}_{{O}}\right)\right)\to \left(\left({a}{{\le }_{{O}}}^{-1}{b}\wedge {b}{{\le }_{{O}}}^{-1}{c}\right)\to {a}{{\le }_{{O}}}^{-1}{c}\right)$
29 3 6 9 13 20 28 isposd ${⊢}{O}\in \mathrm{Poset}\to {D}\in \mathrm{Poset}$