Metamath Proof Explorer

Theorem isarchiofld

Description: Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018)

Ref Expression
Hypotheses isarchiofld.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
isarchiofld.h ⊢ 𝐻 = ( ℤRHom ‘ 𝑊 )
isarchiofld.l ⊢ < = ( lt ‘ 𝑊 )
Assertion isarchiofld ( 𝑊 ∈ oField → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 isarchiofld.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 isarchiofld.h ⊢ 𝐻 = ( ℤRHom ‘ 𝑊 )
3 isarchiofld.l ⊢ < = ( lt ‘ 𝑊 )
4 isofld ⊢ ( 𝑊 ∈ oField ↔ ( 𝑊 ∈ Field ∧ 𝑊 ∈ oRing ) )
5 4 simprbi ⊢ ( 𝑊 ∈ oField → 𝑊 ∈ oRing )
6 orngogrp ⊢ ( 𝑊 ∈ oRing → 𝑊 ∈ oGrp )
7 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
8 eqid ⊢ ( .g ‘ 𝑊 ) = ( .g ‘ 𝑊 )
9 1 7 3 8 isarchi3 ⊢ ( 𝑊 ∈ oGrp → ( 𝑊 ∈ Archi ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ) )
10 5 6 9 3syl ⊢ ( 𝑊 ∈ oField → ( 𝑊 ∈ Archi ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ) )
11 orngring ⊢ ( 𝑊 ∈ oRing → 𝑊 ∈ Ring )
12 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
13 1 12 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
14 5 11 13 3syl ⊢ ( 𝑊 ∈ oField → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
15 breq2 ⊢ ( 𝑦 = ( 1r ‘ 𝑊 ) → ( ( 0g ‘ 𝑊 ) < 𝑦 ↔ ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) ) )
16 oveq2 ⊢ ( 𝑦 = ( 1r ‘ 𝑊 ) → ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
17 16 breq2d ⊢ ( 𝑦 = ( 1r ‘ 𝑊 ) → ( 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ↔ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
18 17 rexbidv ⊢ ( 𝑦 = ( 1r ‘ 𝑊 ) → ( ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
19 15 18 imbi12d ⊢ ( 𝑦 = ( 1r ‘ 𝑊 ) → ( ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ↔ ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ) )
20 19 ralbidv ⊢ ( 𝑦 = ( 1r ‘ 𝑊 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ) )
21 20 rspcv ⊢ ( ( 1r ‘ 𝑊 ) ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) → ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ) )
22 14 21 syl ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) → ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ) )
23 7 12 3 ofldlt1 ⊢ ( 𝑊 ∈ oField → ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) )
24 pm5.5 ⊢ ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ( ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
25 23 24 syl ⊢ ( 𝑊 ∈ oField → ( ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
26 25 ralbidv ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < ( 1r ‘ 𝑊 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
27 22 26 sylibd ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) → ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
28 5 11 syl ⊢ ( 𝑊 ∈ oField → 𝑊 ∈ Ring )
29 nnz ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
30 2 8 12 zrhmulg ⊢ ( ( 𝑊 ∈ Ring ∧ 𝑛 ∈ ℤ ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
31 28 29 30 syl2an ⊢ ( ( 𝑊 ∈ oField ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
32 31 breq2d ⊢ ( ( 𝑊 ∈ oField ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
33 32 rexbidva ⊢ ( 𝑊 ∈ oField → ( ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
34 33 ralbidv ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
35 27 34 sylibrd ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) → ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) )
36 nfv ⊢ Ⅎ 𝑥 𝑊 ∈ oField
37 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 )
38 36 37 nfan ⊢ Ⅎ 𝑥 ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) )
39 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
40 38 39 nfan ⊢ Ⅎ 𝑥 ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 )
41 28 ad3antrrr ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → 𝑊 ∈ Ring )
42 simplrr ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → 𝑥 ∈ 𝐵 )
43 simplrl ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → 𝑦 ∈ 𝐵 )
44 simpr ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( 0g ‘ 𝑊 ) < 𝑦 )
45 simplll ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → 𝑊 ∈ oField )
46 ringgrp ⊢ ( 𝑊 ∈ Ring → 𝑊 ∈ Grp )
47 1 7 grpidcl ⊢ ( 𝑊 ∈ Grp → ( 0g ‘ 𝑊 ) ∈ 𝐵 )
48 41 46 47 3syl ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( 0g ‘ 𝑊 ) ∈ 𝐵 )
49 3 pltne ⊢ ( ( 𝑊 ∈ oField ∧ ( 0g ‘ 𝑊 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0g ‘ 𝑊 ) < 𝑦 → ( 0g ‘ 𝑊 ) ≠ 𝑦 ) )
50 45 48 43 49 syl3anc ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( ( 0g ‘ 𝑊 ) < 𝑦 → ( 0g ‘ 𝑊 ) ≠ 𝑦 ) )
51 44 50 mpd ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( 0g ‘ 𝑊 ) ≠ 𝑦 )
52 51 necomd ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → 𝑦 ≠ ( 0g ‘ 𝑊 ) )
53 4 simplbi ⊢ ( 𝑊 ∈ oField → 𝑊 ∈ Field )
54 isfld ⊢ ( 𝑊 ∈ Field ↔ ( 𝑊 ∈ DivRing ∧ 𝑊 ∈ CRing ) )
55 54 simplbi ⊢ ( 𝑊 ∈ Field → 𝑊 ∈ DivRing )
56 53 55 syl ⊢ ( 𝑊 ∈ oField → 𝑊 ∈ DivRing )
57 eqid ⊢ ( Unit ‘ 𝑊 ) = ( Unit ‘ 𝑊 )
58 1 57 7 drngunit ⊢ ( 𝑊 ∈ DivRing → ( 𝑦 ∈ ( Unit ‘ 𝑊 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) ) )
59 45 56 58 3syl ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( 𝑦 ∈ ( Unit ‘ 𝑊 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) ) )
60 43 52 59 mpbir2and ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → 𝑦 ∈ ( Unit ‘ 𝑊 ) )
61 eqid ⊢ ( /r ‘ 𝑊 ) = ( /r ‘ 𝑊 )
62 1 57 61 dvrcl ⊢ ( ( 𝑊 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( Unit ‘ 𝑊 ) ) → ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
63 41 42 60 62 syl3anc ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
64 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ 𝑧 < ( 𝐻 ‘ 𝑛 ) ) )
65 64 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) ) )
66 65 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) )
67 66 bilani ⊢ ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) )
68 67 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) )
69 breq1 ⊢ ( 𝑧 = ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) → ( 𝑧 < ( 𝐻 ‘ 𝑛 ) ↔ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) )
70 69 rexbidv ⊢ ( 𝑧 = ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) → ( ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) )
71 70 rspcv ⊢ ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 → ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) )
72 63 68 71 sylc ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) )
73 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
74 simp-4l ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ oField )
75 74 5 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ oRing )
76 74 28 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ Ring )
77 simp-4r ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) )
78 77 simprd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑥 ∈ 𝐵 )
79 77 simpld ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑦 ∈ 𝐵 )
80 simpllr ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 0g ‘ 𝑊 ) < 𝑦 )
81 76 46 47 3syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 0g ‘ 𝑊 ) ∈ 𝐵 )
82 74 81 79 49 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 0g ‘ 𝑊 ) < 𝑦 → ( 0g ‘ 𝑊 ) ≠ 𝑦 ) )
83 80 82 mpd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 0g ‘ 𝑊 ) ≠ 𝑦 )
84 83 necomd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑦 ≠ ( 0g ‘ 𝑊 ) )
85 74 56 58 3syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑦 ∈ ( Unit ‘ 𝑊 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) ) )
86 79 84 85 mpbir2and ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑦 ∈ ( Unit ‘ 𝑊 ) )
87 76 78 86 62 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
88 simplr ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑛 ∈ ℕ )
89 74 88 31 syl2anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
90 76 46 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ Grp )
91 88 29 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑛 ∈ ℤ )
92 76 13 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
93 1 8 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ ( 1r ‘ 𝑊 ) ∈ 𝐵 ) → ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
94 90 91 92 93 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
95 89 94 eqeltrd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝐻 ‘ 𝑛 ) ∈ 𝐵 )
96 74 56 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ DivRing )
97 simpr ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) )
98 1 73 7 75 87 95 79 3 96 97 80 orngrmullt ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑦 ) < ( ( 𝐻 ‘ 𝑛 ) ( .r ‘ 𝑊 ) 𝑦 ) )
99 1 57 61 73 dvrcan1 ⊢ ( ( 𝑊 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( Unit ‘ 𝑊 ) ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑥 )
100 76 78 86 99 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑥 )
101 89 oveq1d ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝐻 ‘ 𝑛 ) ( .r ‘ 𝑊 ) 𝑦 ) = ( ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( .r ‘ 𝑊 ) 𝑦 ) )
102 1 8 73 mulgass2 ⊢ ( ( 𝑊 ∈ Ring ∧ ( 𝑛 ∈ ℤ ∧ ( 1r ‘ 𝑊 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) ) )
103 76 91 92 79 102 syl13anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) ) )
104 1 73 12 ringlidm ⊢ ( ( 𝑊 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑦 )
105 76 79 104 syl2anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑦 )
106 105 oveq2d ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑛 ( .g ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) ) = ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
107 101 103 106 3eqtrd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝐻 ‘ 𝑛 ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
108 98 100 107 3brtr3d ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
109 108 ex ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) → 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
110 109 reximdva ⊢ ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
111 110 adantllr ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
112 72 111 mpd ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
113 112 ex ⊢ ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
114 113 expr ⊢ ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 → ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ) )
115 40 114 ralrimi ⊢ ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
116 115 ralrimiva ⊢ ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
117 116 ex ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ) )
118 35 117 impbid ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) )
119 10 118 bitrd ⊢ ( 𝑊 ∈ oField → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) )