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

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 simpr ⊢ ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) → ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) )
65 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ 𝑧 < ( 𝐻 ‘ 𝑛 ) ) )
66 65 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) ) )
67 66 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ↔ ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) )
68 64 67 sylib ⊢ ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) )
69 68 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) )
70 breq1 ⊢ ( 𝑧 = ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) → ( 𝑧 < ( 𝐻 ‘ 𝑛 ) ↔ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) )
71 70 rexbidv ⊢ ( 𝑧 = ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) → ( ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) )
72 71 rspcv ⊢ ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 → ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑧 < ( 𝐻 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) )
73 63 69 72 sylc ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) )
74 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
75 simp-4l ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ oField )
76 75 5 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ oRing )
77 75 28 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ Ring )
78 simp-4r ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) )
79 78 simprd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑥 ∈ 𝐵 )
80 78 simpld ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑦 ∈ 𝐵 )
81 simpllr ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 0g ‘ 𝑊 ) < 𝑦 )
82 77 46 47 3syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 0g ‘ 𝑊 ) ∈ 𝐵 )
83 75 82 80 49 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 0g ‘ 𝑊 ) < 𝑦 → ( 0g ‘ 𝑊 ) ≠ 𝑦 ) )
84 81 83 mpd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 0g ‘ 𝑊 ) ≠ 𝑦 )
85 84 necomd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑦 ≠ ( 0g ‘ 𝑊 ) )
86 75 56 58 3syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑦 ∈ ( Unit ‘ 𝑊 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) ) )
87 80 85 86 mpbir2and ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑦 ∈ ( Unit ‘ 𝑊 ) )
88 77 79 87 62 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
89 simplr ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑛 ∈ ℕ )
90 75 89 31 syl2anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
91 77 46 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ Grp )
92 89 29 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑛 ∈ ℤ )
93 77 13 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
94 1 8 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ ( 1r ‘ 𝑊 ) ∈ 𝐵 ) → ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
95 91 92 93 94 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
96 90 95 eqeltrd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝐻 ‘ 𝑛 ) ∈ 𝐵 )
97 75 56 syl ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑊 ∈ DivRing )
98 simpr ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) )
99 1 74 7 76 88 96 80 3 97 98 81 orngrmullt ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑦 ) < ( ( 𝐻 ‘ 𝑛 ) ( .r ‘ 𝑊 ) 𝑦 ) )
100 1 57 61 74 dvrcan1 ⊢ ( ( 𝑊 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( Unit ‘ 𝑊 ) ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑥 )
101 77 79 87 100 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑥 )
102 90 oveq1d ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝐻 ‘ 𝑛 ) ( .r ‘ 𝑊 ) 𝑦 ) = ( ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( .r ‘ 𝑊 ) 𝑦 ) )
103 1 8 74 mulgass2 ⊢ ( ( 𝑊 ∈ Ring ∧ ( 𝑛 ∈ ℤ ∧ ( 1r ‘ 𝑊 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) ) )
104 77 92 93 80 103 syl13anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝑛 ( .g ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑛 ( .g ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) ) )
105 1 74 12 ringlidm ⊢ ( ( 𝑊 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑦 )
106 77 80 105 syl2anc ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) = 𝑦 )
107 106 oveq2d ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( 𝑛 ( .g ‘ 𝑊 ) ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑦 ) ) = ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
108 102 104 107 3eqtrd ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → ( ( 𝐻 ‘ 𝑛 ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
109 99 101 108 3brtr3d ⊢ ( ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) ) → 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
110 109 ex ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) → 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
111 110 reximdva ⊢ ( ( ( 𝑊 ∈ oField ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
112 111 adantllr ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ( ∃ 𝑛 ∈ ℕ ( 𝑥 ( /r ‘ 𝑊 ) 𝑦 ) < ( 𝐻 ‘ 𝑛 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
113 73 112 mpd ⊢ ( ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) ∧ ( 0g ‘ 𝑊 ) < 𝑦 ) → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) )
114 113 ex ⊢ ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
115 114 expr ⊢ ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 → ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ) )
116 40 115 ralrimi ⊢ ( ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
117 116 ralrimiva ⊢ ( ( 𝑊 ∈ oField ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) )
118 117 ex ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ) )
119 35 118 impbid ⊢ ( 𝑊 ∈ oField → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 0g ‘ 𝑊 ) < 𝑦 → ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝑛 ( .g ‘ 𝑊 ) 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) )
120 10 119 bitrd ⊢ ( 𝑊 ∈ oField → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑛 ∈ ℕ 𝑥 < ( 𝐻 ‘ 𝑛 ) ) )