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

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 10 12 13 mulgnn0cld ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
15 simpl3 ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑦 ∈ 𝐵 )
16 1 4 5 tltnle ⊢ ( ( 𝑊 ∈ Toset ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑛 · 𝑥 ) < 𝑦 ↔ ¬ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) )
17 16 con2bid ⊢ ( ( 𝑊 ∈ Toset ∧ ( 𝑛 · 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ≤ ( 𝑛 · 𝑥 ) ↔ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
18 9 14 15 17 syl3anc ⊢ ( ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 ≤ ( 𝑛 · 𝑥 ) ↔ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
19 18 rexbidva ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ↔ ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
20 19 imbi2d ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
21 1 2 3 5 isinftm ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
22 21 notbid ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ¬ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
23 rexnal ⊢ ( ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ↔ ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 )
24 23 imbi2i ⊢ ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ↔ ( 0 < 𝑥 → ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) )
25 imnan ⊢ ( ( 0 < 𝑥 → ¬ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ↔ ¬ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) )
26 24 25 bitr2i ⊢ ( ¬ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) )
27 22 26 bitrdi ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
28 27 3adant1r ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ ¬ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
29 20 28 bitr4d ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
30 29 3expb ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
31 30 2ralbidva ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ) )
32 8 31 bitr4d ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 ≤ ( 𝑛 · 𝑥 ) ) ) )