This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
isomnd.1 ⊢ + = ( +g ‘ 𝑀 )
isomnd.2 ⊢ ≤ = ( le ‘ 𝑀 )
Assertion isomnd ( 𝑀 ∈ oMnd ↔ ( 𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) )

Proof

Step Hyp Ref Expression
1 isomnd.0 ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 isomnd.1 ⊢ + = ( +g ‘ 𝑀 )
3 isomnd.2 ⊢ ≤ = ( le ‘ 𝑀 )
4 fvexd ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) ∈ V )
5 simpr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → 𝑣 = ( Base ‘ 𝑚 ) )
6 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
7 6 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
8 5 7 eqtrd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → 𝑣 = ( Base ‘ 𝑀 ) )
9 8 1 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → 𝑣 = 𝐵 )
10 raleq ⊢ ( 𝑣 = 𝐵 → ( ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ↔ ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) )
11 10 raleqbi1dv ⊢ ( 𝑣 = 𝐵 → ( ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ↔ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) )
12 11 raleqbi1dv ⊢ ( 𝑣 = 𝐵 → ( ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) )
13 9 12 syl ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → ( ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) )
14 13 anbi2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → ( ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ) )
15 14 sbcbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → ( [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ) )
16 15 sbcbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑣 = ( Base ‘ 𝑚 ) ) → ( [ ( +g ‘ 𝑚 ) / 𝑝 ] [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ [ ( +g ‘ 𝑚 ) / 𝑝 ] [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ) )
17 4 16 sbcied ⊢ ( 𝑚 = 𝑀 → ( [ ( Base ‘ 𝑚 ) / 𝑣 ] [ ( +g ‘ 𝑚 ) / 𝑝 ] [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ [ ( +g ‘ 𝑚 ) / 𝑝 ] [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ) )
18 fvexd ⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) ∈ V )
19 simpr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → 𝑝 = ( +g ‘ 𝑚 ) )
20 fveq2 ⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
21 20 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
22 19 21 eqtrd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → 𝑝 = ( +g ‘ 𝑀 ) )
23 22 2 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → 𝑝 = + )
24 23 oveqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( 𝑎 𝑝 𝑐 ) = ( 𝑎 + 𝑐 ) )
25 23 oveqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( 𝑏 𝑝 𝑐 ) = ( 𝑏 + 𝑐 ) )
26 24 25 breq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ↔ ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) )
27 26 imbi2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ↔ ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) )
28 27 ralbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ↔ ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) )
29 28 2ralbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) )
30 29 anbi2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) ) )
31 30 sbcbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑝 = ( +g ‘ 𝑚 ) ) → ( [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) ) )
32 18 31 sbcied ⊢ ( 𝑚 = 𝑀 → ( [ ( +g ‘ 𝑚 ) / 𝑝 ] [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) ) )
33 fvexd ⊢ ( 𝑚 = 𝑀 → ( le ‘ 𝑚 ) ∈ V )
34 simpr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → 𝑙 = ( le ‘ 𝑚 ) )
35 simpl ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → 𝑚 = 𝑀 )
36 35 fveq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → ( le ‘ 𝑚 ) = ( le ‘ 𝑀 ) )
37 34 36 eqtrd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → 𝑙 = ( le ‘ 𝑀 ) )
38 37 3 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → 𝑙 = ≤ )
39 38 breqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → ( 𝑎 𝑙 𝑏 ↔ 𝑎 ≤ 𝑏 ) )
40 38 breqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → ( ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ↔ ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) )
41 39 40 imbi12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → ( ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ↔ ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) )
42 41 ralbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → ( ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ↔ ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) )
43 42 2ralbidv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) )
44 43 anbi2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑙 = ( le ‘ 𝑚 ) ) → ( ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) ↔ ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) )
45 33 44 sbcied ⊢ ( 𝑚 = 𝑀 → ( [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) ↔ ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) )
46 eleq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ∈ Toset ↔ 𝑀 ∈ Toset ) )
47 46 anbi1d ⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ↔ ( 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) )
48 45 47 bitrd ⊢ ( 𝑚 = 𝑀 → ( [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 𝑙 𝑏 → ( 𝑎 + 𝑐 ) 𝑙 ( 𝑏 + 𝑐 ) ) ) ↔ ( 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) )
49 17 32 48 3bitrd ⊢ ( 𝑚 = 𝑀 → ( [ ( Base ‘ 𝑚 ) / 𝑣 ] [ ( +g ‘ 𝑚 ) / 𝑝 ] [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) ↔ ( 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) )
50 df-omnd ⊢ oMnd = { 𝑚 ∈ Mnd ∣ [ ( Base ‘ 𝑚 ) / 𝑣 ] [ ( +g ‘ 𝑚 ) / 𝑝 ] [ ( le ‘ 𝑚 ) / 𝑙 ] ( 𝑚 ∈ Toset ∧ ∀ 𝑎 ∈ 𝑣 ∀ 𝑏 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ( 𝑎 𝑙 𝑏 → ( 𝑎 𝑝 𝑐 ) 𝑙 ( 𝑏 𝑝 𝑐 ) ) ) }
51 49 50 elrab2 ⊢ ( 𝑀 ∈ oMnd ↔ ( 𝑀 ∈ Mnd ∧ ( 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) )
52 3anass ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ↔ ( 𝑀 ∈ Mnd ∧ ( 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) )
53 51 52 bitr4i ⊢ ( 𝑀 ∈ oMnd ↔ ( 𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) )