Metamath Proof Explorer

Theorem submarchi

Description: A submonoid is archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018)

Ref Expression
Assertion submarchi ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( 𝑊 ↾s 𝐴 ) ∈ Archi )

Proof

Step Hyp Ref Expression
1 submrcl ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → 𝑊 ∈ Mnd )
2 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
4 eqid ⊢ ( .g ‘ 𝑊 ) = ( .g ‘ 𝑊 )
5 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
6 eqid ⊢ ( lt ‘ 𝑊 ) = ( lt ‘ 𝑊 )
7 2 3 4 5 6 isarchi2 ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
8 1 7 sylan2 ⊢ ( ( 𝑊 ∈ Toset ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
9 8 biimpa ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) ∧ 𝑊 ∈ Archi ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) )
10 9 an32s ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) )
11 eqid ⊢ ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s 𝐴 )
12 11 submbas ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → 𝐴 = ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
13 2 submss ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → 𝐴 ⊆ ( Base ‘ 𝑊 ) )
14 12 13 eqsstrrd ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑊 ) )
15 ssralv ⊢ ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑊 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) → ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
16 15 ralimdv ⊢ ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑊 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
17 ssralv ⊢ ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑊 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
18 16 17 syld ⊢ ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝑊 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
19 14 18 syl ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
20 19 adantl ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ) )
21 11 3 subm0 ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( 0g ‘ 𝑊 ) = ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) )
22 21 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) → ( 0g ‘ 𝑊 ) = ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) )
23 11 5 ressle ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( le ‘ 𝑊 ) = ( le ‘ ( 𝑊 ↾s 𝐴 ) ) )
24 23 difeq1d ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( ( le ‘ 𝑊 ) ∖ I ) = ( ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ∖ I ) )
25 5 6 pltfval ⊢ ( 𝑊 ∈ Mnd → ( lt ‘ 𝑊 ) = ( ( le ‘ 𝑊 ) ∖ I ) )
26 1 25 syl ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( lt ‘ 𝑊 ) = ( ( le ‘ 𝑊 ) ∖ I ) )
27 11 submmnd ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( 𝑊 ↾s 𝐴 ) ∈ Mnd )
28 eqid ⊢ ( le ‘ ( 𝑊 ↾s 𝐴 ) ) = ( le ‘ ( 𝑊 ↾s 𝐴 ) )
29 eqid ⊢ ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( lt ‘ ( 𝑊 ↾s 𝐴 ) )
30 28 29 pltfval ⊢ ( ( 𝑊 ↾s 𝐴 ) ∈ Mnd → ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ∖ I ) )
31 27 30 syl ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ∖ I ) )
32 24 26 31 3eqtr4d ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( lt ‘ 𝑊 ) = ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) )
33 32 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) → ( lt ‘ 𝑊 ) = ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) )
34 eqidd ⊢ ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) → 𝑥 = 𝑥 )
35 22 33 34 breq123d ⊢ ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) → ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ↔ ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) )
36 eqidd ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑦 = 𝑦 )
37 23 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( le ‘ 𝑊 ) = ( le ‘ ( 𝑊 ↾s 𝐴 ) ) )
38 simplll ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ( SubMnd ‘ 𝑊 ) )
39 simpr ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
40 39 nnnn0d ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
41 simpllr ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
42 38 12 syl ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 = ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
43 41 42 eleqtrrd ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ 𝐴 )
44 eqid ⊢ ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) = ( .g ‘ ( 𝑊 ↾s 𝐴 ) )
45 4 11 44 submmulg ⊢ ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) = ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) )
46 38 40 43 45 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) = ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) )
47 36 37 46 breq123d ⊢ ( ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ↔ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) )
48 47 rexbidva ⊢ ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) → ( ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) )
49 35 48 imbi12d ⊢ ( ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) → ( ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ↔ ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
50 49 ralbidva ⊢ ( ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) → ( ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
51 50 ralbidva ⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑊 ) → ( ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
52 51 adantl ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
53 20 52 sylibd ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ 𝑊 ) ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
54 10 53 mpd ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) )
55 resstos ⊢ ( ( 𝑊 ∈ Toset ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( 𝑊 ↾s 𝐴 ) ∈ Toset )
56 27 adantl ⊢ ( ( 𝑊 ∈ Toset ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( 𝑊 ↾s 𝐴 ) ∈ Mnd )
57 eqid ⊢ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) = ( Base ‘ ( 𝑊 ↾s 𝐴 ) )
58 eqid ⊢ ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) = ( 0g ‘ ( 𝑊 ↾s 𝐴 ) )
59 57 58 44 28 29 isarchi2 ⊢ ( ( ( 𝑊 ↾s 𝐴 ) ∈ Toset ∧ ( 𝑊 ↾s 𝐴 ) ∈ Mnd ) → ( ( 𝑊 ↾s 𝐴 ) ∈ Archi ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
60 55 56 59 syl2anc ⊢ ( ( 𝑊 ∈ Toset ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( ( 𝑊 ↾s 𝐴 ) ∈ Archi ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
61 60 adantlr ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( ( 𝑊 ↾s 𝐴 ) ∈ Archi ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ( ( 0g ‘ ( 𝑊 ↾s 𝐴 ) ) ( lt ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ( le ‘ ( 𝑊 ↾s 𝐴 ) ) ( 𝑛 ( .g ‘ ( 𝑊 ↾s 𝐴 ) ) 𝑥 ) ) ) )
62 54 61 mpbird ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Archi ) ∧ 𝐴 ∈ ( SubMnd ‘ 𝑊 ) ) → ( 𝑊 ↾s 𝐴 ) ∈ Archi )