Proof of Theorem isarchi2
Step | Hyp | Ref
| Expression |
1 | | isarchi2.b |
. . . 4
⊢ 𝐵 = (Base‘𝑊) |
2 | | isarchi2.0 |
. . . 4
⊢ 0 =
(0g‘𝑊) |
3 | | eqid 2732 |
. . . 4
⊢
(⋘‘𝑊) =
(⋘‘𝑊) |
4 | 1, 2, 3 | isarchi 32315 |
. . 3
⊢ (𝑊 ∈ Toset → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑥(⋘‘𝑊)𝑦)) |
5 | 4 | adantr 481 |
. 2
⊢ ((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑥(⋘‘𝑊)𝑦)) |
6 | | simpl1l 1224 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ Toset) |
7 | | isarchi2.x |
. . . . . . . . 9
⊢ · =
(.g‘𝑊) |
8 | | simpl1r 1225 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ Mnd) |
9 | | simpr 485 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
10 | 9 | nnnn0d 12528 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
11 | | simpl2 1192 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ 𝐵) |
12 | 1, 7, 8, 10, 11 | mulgnn0cld 18969 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝑛 · 𝑥) ∈ 𝐵) |
13 | | simpl3 1193 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ 𝐵) |
14 | | isarchi2.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝑊) |
15 | | isarchi2.t |
. . . . . . . . . 10
⊢ < =
(lt‘𝑊) |
16 | 1, 14, 15 | tltnle 18371 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Toset ∧ (𝑛 · 𝑥) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑛 · 𝑥) < 𝑦 ↔ ¬ 𝑦 ≤ (𝑛 · 𝑥))) |
17 | 16 | con2bid 354 |
. . . . . . . 8
⊢ ((𝑊 ∈ Toset ∧ (𝑛 · 𝑥) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑦 ≤ (𝑛 · 𝑥) ↔ ¬ (𝑛 · 𝑥) < 𝑦)) |
18 | 6, 12, 13, 17 | syl3anc 1371 |
. . . . . . 7
⊢ ((((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝑦 ≤ (𝑛 · 𝑥) ↔ ¬ (𝑛 · 𝑥) < 𝑦)) |
19 | 18 | rexbidva 3176 |
. . . . . 6
⊢ (((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (∃𝑛 ∈ ℕ 𝑦 ≤ (𝑛 · 𝑥) ↔ ∃𝑛 ∈ ℕ ¬ (𝑛 · 𝑥) < 𝑦)) |
20 | 19 | imbi2d 340 |
. . . . 5
⊢ (((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 ≤ (𝑛 · 𝑥)) ↔ ( 0 < 𝑥 → ∃𝑛 ∈ ℕ ¬ (𝑛 · 𝑥) < 𝑦))) |
21 | 1, 2, 7, 15 | isinftm 32314 |
. . . . . . . 8
⊢ ((𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(⋘‘𝑊)𝑦 ↔ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))) |
22 | 21 | notbid 317 |
. . . . . . 7
⊢ ((𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (¬ 𝑥(⋘‘𝑊)𝑦 ↔ ¬ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦))) |
23 | | rexnal 3100 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ ¬ (𝑛 · 𝑥) < 𝑦 ↔ ¬ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦) |
24 | 23 | imbi2i 335 |
. . . . . . . 8
⊢ (( 0 < 𝑥 → ∃𝑛 ∈ ℕ ¬ (𝑛 · 𝑥) < 𝑦) ↔ ( 0 < 𝑥 → ¬ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦)) |
25 | | imnan 400 |
. . . . . . . 8
⊢ (( 0 < 𝑥 → ¬ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦) ↔ ¬ ( 0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦)) |
26 | 24, 25 | bitr2i 275 |
. . . . . . 7
⊢ (¬ (
0 < 𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑥) < 𝑦) ↔ ( 0 < 𝑥 → ∃𝑛 ∈ ℕ ¬ (𝑛 · 𝑥) < 𝑦)) |
27 | 22, 26 | bitrdi 286 |
. . . . . 6
⊢ ((𝑊 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (¬ 𝑥(⋘‘𝑊)𝑦 ↔ ( 0 < 𝑥 → ∃𝑛 ∈ ℕ ¬ (𝑛 · 𝑥) < 𝑦))) |
28 | 27 | 3adant1r 1177 |
. . . . 5
⊢ (((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (¬ 𝑥(⋘‘𝑊)𝑦 ↔ ( 0 < 𝑥 → ∃𝑛 ∈ ℕ ¬ (𝑛 · 𝑥) < 𝑦))) |
29 | 20, 28 | bitr4d 281 |
. . . 4
⊢ (((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 ≤ (𝑛 · 𝑥)) ↔ ¬ 𝑥(⋘‘𝑊)𝑦)) |
30 | 29 | 3expb 1120 |
. . 3
⊢ (((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 ≤ (𝑛 · 𝑥)) ↔ ¬ 𝑥(⋘‘𝑊)𝑦)) |
31 | 30 | 2ralbidva 3216 |
. 2
⊢ ((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 ≤ (𝑛 · 𝑥)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑥(⋘‘𝑊)𝑦)) |
32 | 5, 31 | bitr4d 281 |
1
⊢ ((𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd) → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃𝑛 ∈ ℕ 𝑦 ≤ (𝑛 · 𝑥)))) |