Metamath Proof Explorer

Theorem isarchi3

Description: This is the usual definition of the Archimedean property for an ordered group. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isarchi3.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
isarchi3.0 ⊢ 0 = ( 0g ‘ 𝑊 )
isarchi3.i ⊢ < = ( lt ‘ 𝑊 )
isarchi3.x ⊢ · = ( .g ‘ 𝑊 )
Assertion isarchi3 ( 𝑊 ∈ oGrp → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 isarchi3.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 isarchi3.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 isarchi3.i ⊢ < = ( lt ‘ 𝑊 )
4 isarchi3.x ⊢ · = ( .g ‘ 𝑊 )
5 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
6 5 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
7 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
8 6 7 syl ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Toset )
9 grpmnd ⊢ ( 𝑊 ∈ Grp → 𝑊 ∈ Mnd )
10 9 adantr ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) → 𝑊 ∈ Mnd )
11 5 10 sylbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Mnd )
12 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
13 1 2 4 12 3 isarchi2 ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) ) )
14 8 11 13 syl2anc ⊢ ( 𝑊 ∈ oGrp → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) ) )
15 simpr ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
16 15 adantr ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 𝑛 ∈ ℕ )
17 16 peano2nnd ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( 𝑛 + 1 ) ∈ ℕ )
18 simp-4l ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ oGrp )
19 18 adantr ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 𝑊 ∈ oGrp )
20 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
21 1 2 grpidcl ⊢ ( 𝑊 ∈ Grp → 0 ∈ 𝐵 )
22 19 20 21 3syl ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 0 ∈ 𝐵 )
23 simp-4r ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ 𝐵 )
24 23 adantr ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 𝑥 ∈ 𝐵 )
25 20 ad4antr ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ Grp )
26 15 nnzd ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
27 1 4 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
28 25 26 23 27 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
29 28 adantr ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
30 simpllr ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 0 < 𝑥 )
31 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
32 1 3 31 ogrpaddlt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ) ∧ 0 < 𝑥 ) → ( 0 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) < ( 𝑥 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
33 19 22 24 29 30 32 syl131anc ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( 0 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) < ( 𝑥 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
34 19 20 syl ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 𝑊 ∈ Grp )
35 1 31 2 grplid ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) = ( 𝑛 · 𝑥 ) )
36 34 29 35 syl2anc ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( 0 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) = ( 𝑛 · 𝑥 ) )
37 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
38 ax-1cn ⊢ 1 ∈ ℂ
39 addcom ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑛 + 1 ) = ( 1 + 𝑛 ) )
40 37 38 39 sylancl ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) = ( 1 + 𝑛 ) )
41 40 oveq1d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 + 1 ) · 𝑥 ) = ( ( 1 + 𝑛 ) · 𝑥 ) )
42 16 41 syl ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( ( 𝑛 + 1 ) · 𝑥 ) = ( ( 1 + 𝑛 ) · 𝑥 ) )
43 grpsgrp ⊢ ( 𝑊 ∈ Grp → 𝑊 ∈ Smgrp )
44 19 20 43 3syl ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 𝑊 ∈ Smgrp )
45 1nn ⊢ 1 ∈ ℕ
46 45 a1i ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 1 ∈ ℕ )
47 1 4 31 mulgnndir ⊢ ( ( 𝑊 ∈ Smgrp ∧ ( 1 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 1 + 𝑛 ) · 𝑥 ) = ( ( 1 · 𝑥 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
48 44 46 16 24 47 syl13anc ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( ( 1 + 𝑛 ) · 𝑥 ) = ( ( 1 · 𝑥 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
49 1 4 mulg1 ⊢ ( 𝑥 ∈ 𝐵 → ( 1 · 𝑥 ) = 𝑥 )
50 24 49 syl ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( 1 · 𝑥 ) = 𝑥 )
51 50 oveq1d ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( ( 1 · 𝑥 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) = ( 𝑥 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
52 42 48 51 3eqtrrd ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) = ( ( 𝑛 + 1 ) · 𝑥 ) )
53 33 36 52 3brtr3d ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ( 𝑛 · 𝑥 ) < ( ( 𝑛 + 1 ) · 𝑥 ) )
54 tospos ⊢ ( 𝑊 ∈ Toset → 𝑊 ∈ Poset )
55 18 8 54 3syl ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ Poset )
56 simpllr ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → 𝑦 ∈ 𝐵 )
57 26 peano2zd ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℤ )
58 1 4 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑛 + 1 ) ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑛 + 1 ) · 𝑥 ) ∈ 𝐵 )
59 25 57 23 58 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) · 𝑥 ) ∈ 𝐵 )
60 1 12 3 plelttr ⊢ ( ( 𝑊 ∈ Poset ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ∧ ( ( 𝑛 + 1 ) · 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ∧ ( 𝑛 · 𝑥 ) < ( ( 𝑛 + 1 ) · 𝑥 ) ) → 𝑦 < ( ( 𝑛 + 1 ) · 𝑥 ) ) )
61 55 56 28 59 60 syl13anc ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ∧ ( 𝑛 · 𝑥 ) < ( ( 𝑛 + 1 ) · 𝑥 ) ) → 𝑦 < ( ( 𝑛 + 1 ) · 𝑥 ) ) )
62 61 impl ⊢ ( ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) ∧ ( 𝑛 · 𝑥 ) < ( ( 𝑛 + 1 ) · 𝑥 ) ) → 𝑦 < ( ( 𝑛 + 1 ) · 𝑥 ) )
63 53 62 mpdan ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → 𝑦 < ( ( 𝑛 + 1 ) · 𝑥 ) )
64 oveq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 · 𝑥 ) = ( ( 𝑛 + 1 ) · 𝑥 ) )
65 64 breq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑦 < ( 𝑚 · 𝑥 ) ↔ 𝑦 < ( ( 𝑛 + 1 ) · 𝑥 ) ) )
66 65 rspcev ⊢ ( ( ( 𝑛 + 1 ) ∈ ℕ ∧ 𝑦 < ( ( 𝑛 + 1 ) · 𝑥 ) ) → ∃ 𝑚 ∈ ℕ 𝑦 < ( 𝑚 · 𝑥 ) )
67 17 63 66 syl2anc ⊢ ( ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ∃ 𝑚 ∈ ℕ 𝑦 < ( 𝑚 · 𝑥 ) )
68 67 r19.29an ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ∃ 𝑚 ∈ ℕ 𝑦 < ( 𝑚 · 𝑥 ) )
69 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 𝑥 ) = ( 𝑛 · 𝑥 ) )
70 69 breq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑦 < ( 𝑚 · 𝑥 ) ↔ 𝑦 < ( 𝑛 · 𝑥 ) ) )
71 70 cbvrexvw ⊢ ( ∃ 𝑚 ∈ ℕ 𝑦 < ( 𝑚 · 𝑥 ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) )
72 68 71 sylib ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) )
73 12 3 pltle ⊢ ( ( 𝑊 ∈ oGrp ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ) → ( 𝑦 < ( 𝑛 · 𝑥 ) → 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
74 18 56 28 73 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < ( 𝑛 · 𝑥 ) → 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
75 74 reximdva ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) → ( ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) )
76 75 imp ⊢ ( ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) ∧ ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) )
77 72 76 impbida ⊢ ( ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 0 < 𝑥 ) → ( ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) )
78 77 pm5.74da ⊢ ( ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) ) )
79 78 ralbidva ⊢ ( ( 𝑊 ∈ oGrp ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) ) )
80 79 ralbidva ⊢ ( 𝑊 ∈ oGrp → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 · 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) ) )
81 14 80 bitrd ⊢ ( 𝑊 ∈ oGrp → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) ) )