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 ⊢B=BaseW
isarchi2.0 ⊢0˙=0W
isarchi2.x ⊢·˙=⋅W
isarchi2.l ⊢≤˙=≤W
isarchi2.t ⊢<˙=<W
Assertion isarchi2 ⊢W∈Toset∧W∈Mnd→W∈Archi↔∀x∈B∀y∈B0˙<˙x→∃n∈ℕy≤˙n·˙x

Proof

Step Hyp Ref Expression
1 isarchi2.b ⊢B=BaseW
2 isarchi2.0 ⊢0˙=0W
3 isarchi2.x ⊢·˙=⋅W
4 isarchi2.l ⊢≤˙=≤W
5 isarchi2.t ⊢<˙=<W
6 eqid ⊢⋘⁡W=⋘⁡W
7 1 2 6 isarchi ⊢W∈Toset→W∈Archi↔∀x∈B∀y∈B¬x⋘⁡Wy
8 7 adantr ⊢W∈Toset∧W∈Mnd→W∈Archi↔∀x∈B∀y∈B¬x⋘⁡Wy
9 simpl1l ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→W∈Toset
10 simpl1r ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→W∈Mnd
11 simpr ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→n∈ℕ
12 11 nnnn0d ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→n∈ℕ0
13 simpl2 ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→x∈B
14 1 3 10 12 13 mulgnn0cld ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→n·˙x∈B
15 simpl3 ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→y∈B
16 1 4 5 tltnle ⊢W∈Toset∧n·˙x∈B∧y∈B→n·˙x<˙y↔¬y≤˙n·˙x
17 16 con2bid ⊢W∈Toset∧n·˙x∈B∧y∈B→y≤˙n·˙x↔¬n·˙x<˙y
18 9 14 15 17 syl3anc ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B∧n∈ℕ→y≤˙n·˙x↔¬n·˙x<˙y
19 18 rexbidva ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B→∃n∈ℕy≤˙n·˙x↔∃n∈ℕ¬n·˙x<˙y
20 19 imbi2d ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B→0˙<˙x→∃n∈ℕy≤˙n·˙x↔0˙<˙x→∃n∈ℕ¬n·˙x<˙y
21 1 2 3 5 isinftm ⊢W∈Toset∧x∈B∧y∈B→x⋘⁡Wy↔0˙<˙x∧∀n∈ℕn·˙x<˙y
22 21 notbid ⊢W∈Toset∧x∈B∧y∈B→¬x⋘⁡Wy↔¬0˙<˙x∧∀n∈ℕn·˙x<˙y
23 rexnal ⊢∃n∈ℕ¬n·˙x<˙y↔¬∀n∈ℕn·˙x<˙y
24 23 imbi2i ⊢0˙<˙x→∃n∈ℕ¬n·˙x<˙y↔0˙<˙x→¬∀n∈ℕn·˙x<˙y
25 imnan ⊢0˙<˙x→¬∀n∈ℕn·˙x<˙y↔¬0˙<˙x∧∀n∈ℕn·˙x<˙y
26 24 25 bitr2i ⊢¬0˙<˙x∧∀n∈ℕn·˙x<˙y↔0˙<˙x→∃n∈ℕ¬n·˙x<˙y
27 22 26 bitrdi ⊢W∈Toset∧x∈B∧y∈B→¬x⋘⁡Wy↔0˙<˙x→∃n∈ℕ¬n·˙x<˙y
28 27 3adant1r ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B→¬x⋘⁡Wy↔0˙<˙x→∃n∈ℕ¬n·˙x<˙y
29 20 28 bitr4d ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B→0˙<˙x→∃n∈ℕy≤˙n·˙x↔¬x⋘⁡Wy
30 29 3expb ⊢W∈Toset∧W∈Mnd∧x∈B∧y∈B→0˙<˙x→∃n∈ℕy≤˙n·˙x↔¬x⋘⁡Wy
31 30 2ralbidva ⊢W∈Toset∧W∈Mnd→∀x∈B∀y∈B0˙<˙x→∃n∈ℕy≤˙n·˙x↔∀x∈B∀y∈B¬x⋘⁡Wy
32 8 31 bitr4d ⊢W∈Toset∧W∈Mnd→W∈Archi↔∀x∈B∀y∈B0˙<˙x→∃n∈ℕy≤˙n·˙x