Metamath Proof Explorer

Theorem isomnd

Description: A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isomnd.0 ${⊢}{B}={\mathrm{Base}}_{{M}}$
isomnd.1
isomnd.2
Assertion isomnd

Proof

Step Hyp Ref Expression
1 isomnd.0 ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 isomnd.1
3 isomnd.2
4 fvexd ${⊢}{m}={M}\to {\mathrm{Base}}_{{m}}\in \mathrm{V}$
5 simpr ${⊢}\left({m}={M}\wedge {v}={\mathrm{Base}}_{{m}}\right)\to {v}={\mathrm{Base}}_{{m}}$
6 fveq2 ${⊢}{m}={M}\to {\mathrm{Base}}_{{m}}={\mathrm{Base}}_{{M}}$
7 6 adantr ${⊢}\left({m}={M}\wedge {v}={\mathrm{Base}}_{{m}}\right)\to {\mathrm{Base}}_{{m}}={\mathrm{Base}}_{{M}}$
8 5 7 eqtrd ${⊢}\left({m}={M}\wedge {v}={\mathrm{Base}}_{{m}}\right)\to {v}={\mathrm{Base}}_{{M}}$
9 8 1 eqtr4di ${⊢}\left({m}={M}\wedge {v}={\mathrm{Base}}_{{m}}\right)\to {v}={B}$
10 raleq ${⊢}{v}={B}\to \left(\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)↔\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)\right)$
11 10 raleqbi1dv ${⊢}{v}={B}\to \left(\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)↔\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)\right)$
12 11 raleqbi1dv ${⊢}{v}={B}\to \left(\forall {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)\right)$
13 9 12 syl ${⊢}\left({m}={M}\wedge {v}={\mathrm{Base}}_{{m}}\right)\to \left(\forall {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)\right)$
14 13 anbi2d ${⊢}\left({m}={M}\wedge {v}={\mathrm{Base}}_{{m}}\right)\to \left(\left({m}\in \mathrm{Toset}\wedge \forall {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\forall {c}\in {v}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)\right)↔\left({m}\in \mathrm{Toset}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left({a}{l}{b}\to \left({a}{p}{c}\right){l}\left({b}{p}{c}\right)\right)\right)\right)$
15 14 sbcbidv
16 15 sbcbidv
17 4 16 sbcied
18 fvexd ${⊢}{m}={M}\to {+}_{{m}}\in \mathrm{V}$
19 simpr ${⊢}\left({m}={M}\wedge {p}={+}_{{m}}\right)\to {p}={+}_{{m}}$
20 fveq2 ${⊢}{m}={M}\to {+}_{{m}}={+}_{{M}}$
21 20 adantr ${⊢}\left({m}={M}\wedge {p}={+}_{{m}}\right)\to {+}_{{m}}={+}_{{M}}$
22 19 21 eqtrd ${⊢}\left({m}={M}\wedge {p}={+}_{{m}}\right)\to {p}={+}_{{M}}$
23 22 2 eqtr4di
24 23 oveqd
25 23 oveqd
26 24 25 breq12d
27 26 imbi2d
28 27 ralbidv
29 28 2ralbidv
30 29 anbi2d
31 30 sbcbidv
32 18 31 sbcied
33 fvexd ${⊢}{m}={M}\to {\le }_{{m}}\in \mathrm{V}$
34 simpr ${⊢}\left({m}={M}\wedge {l}={\le }_{{m}}\right)\to {l}={\le }_{{m}}$
35 simpl ${⊢}\left({m}={M}\wedge {l}={\le }_{{m}}\right)\to {m}={M}$
36 35 fveq2d ${⊢}\left({m}={M}\wedge {l}={\le }_{{m}}\right)\to {\le }_{{m}}={\le }_{{M}}$
37 34 36 eqtrd ${⊢}\left({m}={M}\wedge {l}={\le }_{{m}}\right)\to {l}={\le }_{{M}}$
38 37 3 eqtr4di
39 38 breqd
40 38 breqd
41 39 40 imbi12d
42 41 ralbidv
43 42 2ralbidv
44 43 anbi2d
45 33 44 sbcied
46 eleq1 ${⊢}{m}={M}\to \left({m}\in \mathrm{Toset}↔{M}\in \mathrm{Toset}\right)$
47 46 anbi1d
48 45 47 bitrd
49 17 32 48 3bitrd
50 df-omnd
51 49 50 elrab2
52 3anass
53 51 52 bitr4i