Metamath Proof Explorer

Theorem isarchi2

Description: Alternative way to express the predicate " W is Archimedean ", for Tosets. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isarchi2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
isarchi2.0 ⊢ 0 = ( 0g ‘ 𝑊 )
isarchi2.x ⊢ · = ( .g ‘ 𝑊 )
isarchi2.l ⊢ ≤ = ( le ‘ 𝑊 )
isarchi2.t ⊢ < = ( lt ‘ 𝑊 )
Assertion isarchi2 ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 isarchi2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 isarchi2.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 isarchi2.x ⊢ · = ( .g ‘ 𝑊 )
4 isarchi2.l ⊢ ≤ = ( le ‘ 𝑊 )
5 isarchi2.t ⊢ < = ( lt ‘ 𝑊 )
6 eqid ⊢ ( ⋘ ‘ 𝑊 ) = ( ⋘ ‘ 𝑊 )
7 1 2 6 isarchi ⊢ ( 𝑊 ∈ Toset → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
8 7 adantr ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
9 simpl1l ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ Toset )
10 simpl1r ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ Mnd )
11 simpr ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
12 11 nnnn0d ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
13 simpl2 ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ 𝐵 )
14 1 3 mulgnn0cl ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
15 10 12 13 14 syl3anc ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
16 simpl3 ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑦 ∈ 𝐵 )
17 1 4 5 tltnle ⊢ ( ( 𝑊 ∈ Toset ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑛 · 𝑥 ) < 𝑦 ↔ ¬ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) )
18 17 con2bid ⊢ ( ( 𝑊 ∈ Toset ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ≤ ( 𝑛 · 𝑥 ) ↔ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
19 9 15 16 18 syl3anc ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 ≤ ( 𝑛 · 𝑥 ) ↔ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
20 19 rexbidva ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ↔ ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
21 20 imbi2d ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
22 1 2 3 5 isinftm ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
23 22 notbid ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ¬ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
24 rexnal ⊢ ( ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ↔ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 )
25 24 imbi2i ⊢ ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ↔ ( 0 < 𝑥 → ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) )
26 imnan ⊢ ( ( 0 < 𝑥 → ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ↔ ¬ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) )
27 25 26 bitr2i ⊢ ( ¬ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
28 23 27 bitrdi ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
29 28 3adant1r ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
30 21 29 bitr4d ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
31 30 3expb ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
32 31 2ralbidva ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
33 8 32 bitr4d ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ) )