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

Metamath Proof Explorer

Theorem archiabl

Description: Archimedean left- and right- ordered groups are Abelian. (Contributed by Thierry Arnoux, 1-May-2018)

Ref Expression
Assertion archiabl ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) → 𝑊 ∈ Abel )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
3 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
4 eqid ⊢ ( lt ‘ 𝑊 ) = ( lt ‘ 𝑊 )
5 eqid ⊢ ( .g ‘ 𝑊 ) = ( .g ‘ 𝑊 )
6 simpll1 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ oGrp )
7 simpll3 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Archi )
8 simplr ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
9 simprl ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 )
10 simp2 ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
11 simp1rr ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) )
12 simp3 ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 )
13 breq2 ⊢ ( 𝑥 = 𝑦 → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ↔ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) )
14 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑣 ( le ‘ 𝑊 ) 𝑥 ↔ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
15 13 14 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 → 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
16 15 rspcv ⊢ ( 𝑦 ∈ ( Base ‘ 𝑊 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 → 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
17 10 11 12 16 syl3c ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ) → 𝑣 ( le ‘ 𝑊 ) 𝑦 )
18 1 2 3 4 5 6 7 8 9 17 archiabllem1 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
19 18 adantllr ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
20 simpr ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
21 breq2 ⊢ ( 𝑢 = 𝑣 → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ↔ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) )
22 breq1 ⊢ ( 𝑢 = 𝑣 → ( 𝑢 ( le ‘ 𝑊 ) 𝑥 ↔ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) )
23 22 imbi2d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
24 23 ralbidv ⊢ ( 𝑢 = 𝑣 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
25 21 24 anbi12d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) )
26 25 cbvrexvw ⊢ ( ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
27 20 26 sylib ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
28 19 27 r19.29a ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
29 simpl1 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ oGrp )
30 simpl3 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Archi )
31 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
32 simpl2 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ( oppg ‘ 𝑊 ) ∈ oGrp )
33 simpr ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
34 ralnex ⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
35 33 34 sylibr ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
36 rexanali ⊢ ( ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) )
37 36 imbi2i ⊢ ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
38 imnan ⊢ ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
39 37 38 bitri ⊢ ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
40 39 ralbii ⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ¬ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
41 35 40 sylibr ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) )
42 22 notbid ⊢ ( 𝑢 = 𝑣 → ( ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ↔ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) )
43 42 anbi2d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
44 43 rexbidv ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
45 21 44 imbi12d ⊢ ( 𝑢 = 𝑣 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) ) )
46 45 cbvralvw ⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
47 41 46 sylib ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → ∀ 𝑣 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
48 47 r19.21bi ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ) )
49 14 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ↔ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
50 13 49 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
51 50 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑥 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
52 48 51 imbitrdi ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 → ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ) )
53 52 3impia ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
54 simp1l1 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → 𝑊 ∈ oGrp )
55 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
56 55 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
57 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
58 54 56 57 3syl ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → 𝑊 ∈ Toset )
59 simp2 ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
60 1 3 4 tltnle ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑦 ( lt ‘ 𝑊 ) 𝑣 ↔ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) )
61 60 bicomd ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
62 61 3com23 ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
63 62 3expa ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
64 63 anbi2d ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) ) )
65 64 rexbidva ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) ) )
66 58 59 65 syl2anc ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ ¬ 𝑣 ( le ‘ 𝑊 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) ) )
67 53 66 mpbid ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑣 ) → ∃ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝑊 ) 𝑣 ) )
68 1 2 3 4 5 29 30 31 32 67 archiabllem2 ⊢ ( ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ¬ ∃ 𝑢 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑢 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → 𝑢 ( le ‘ 𝑊 ) 𝑥 ) ) ) → 𝑊 ∈ Abel )
69 28 68 pm2.61dan ⊢ ( ( 𝑊 ∈ oGrp ∧ ( oppg ‘ 𝑊 ) ∈ oGrp ∧ 𝑊 ∈ Archi ) → 𝑊 ∈ Abel )