Step | Hyp | Ref
| Expression |
1 | | znle2.y |
. . . . 5
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
2 | | fvex 6113 |
. . . . 5
⊢
(ℤ/nℤ‘𝑁) ∈ V |
3 | 1, 2 | eqeltri 2684 |
. . . 4
⊢ 𝑌 ∈ V |
4 | 3 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
V) |
5 | | znleval.x |
. . . 4
⊢ 𝑋 = (Base‘𝑌) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝑋 =
(Base‘𝑌)) |
7 | | znle2.l |
. . . 4
⊢ ≤ =
(le‘𝑌) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ≤ = (le‘𝑌)) |
9 | | znle2.f |
. . . . . . . . . 10
⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) |
10 | | znle2.w |
. . . . . . . . . 10
⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) |
11 | 1, 5, 9, 10 | znf1o 19719 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝑋) |
12 | | f1ocnv 6062 |
. . . . . . . . 9
⊢ (𝐹:𝑊–1-1-onto→𝑋 → ◡𝐹:𝑋–1-1-onto→𝑊) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋–1-1-onto→𝑊) |
14 | | f1of 6050 |
. . . . . . . 8
⊢ (◡𝐹:𝑋–1-1-onto→𝑊 → ◡𝐹:𝑋⟶𝑊) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋⟶𝑊) |
16 | | sseq1 3589 |
. . . . . . . . . 10
⊢ (ℤ
= if(𝑁 = 0, ℤ,
(0..^𝑁)) → (ℤ
⊆ ℤ ↔ if(𝑁
= 0, ℤ, (0..^𝑁))
⊆ ℤ)) |
17 | | sseq1 3589 |
. . . . . . . . . 10
⊢
((0..^𝑁) = if(𝑁 = 0, ℤ, (0..^𝑁)) → ((0..^𝑁) ⊆ ℤ ↔
if(𝑁 = 0, ℤ,
(0..^𝑁)) ⊆
ℤ)) |
18 | | ssid 3587 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℤ |
19 | | elfzoelz 12339 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) |
20 | 19 | ssriv 3572 |
. . . . . . . . . 10
⊢
(0..^𝑁) ⊆
ℤ |
21 | 16, 17, 18, 20 | keephyp 4102 |
. . . . . . . . 9
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆
ℤ |
22 | 10, 21 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑊 ⊆
ℤ |
23 | | zssre 11261 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
24 | 22, 23 | sstri 3577 |
. . . . . . 7
⊢ 𝑊 ⊆
ℝ |
25 | | fss 5969 |
. . . . . . 7
⊢ ((◡𝐹:𝑋⟶𝑊 ∧ 𝑊 ⊆ ℝ) → ◡𝐹:𝑋⟶ℝ) |
26 | 15, 24, 25 | sylancl 693 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋⟶ℝ) |
27 | 26 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (◡𝐹‘𝑥) ∈ ℝ) |
28 | 27 | leidd 10473 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑥)) |
29 | 1, 9, 10, 7, 5 | znleval2 19723 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥 ≤ 𝑥 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑥))) |
30 | 29 | 3anidm23 1377 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (𝑥 ≤ 𝑥 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑥))) |
31 | 28, 30 | mpbird 246 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → 𝑥 ≤ 𝑥) |
32 | 1, 9, 10, 7, 5 | znleval2 19723 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ≤ 𝑦 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦))) |
33 | 1, 9, 10, 7, 5 | znleval2 19723 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑦 ≤ 𝑥 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥))) |
34 | 33 | 3com23 1263 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑦 ≤ 𝑥 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥))) |
35 | 32, 34 | anbi12d 743 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥)))) |
36 | 27 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (◡𝐹‘𝑥) ∈ ℝ) |
37 | 26 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑦 ∈ 𝑋) → (◡𝐹‘𝑦) ∈ ℝ) |
38 | 37 | 3adant2 1073 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (◡𝐹‘𝑦) ∈ ℝ) |
39 | 36, 38 | letri3d 10058 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥)))) |
40 | | f1of1 6049 |
. . . . . . . 8
⊢ (◡𝐹:𝑋–1-1-onto→𝑊 → ◡𝐹:𝑋–1-1→𝑊) |
41 | 13, 40 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋–1-1→𝑊) |
42 | | f1fveq 6420 |
. . . . . . 7
⊢ ((◡𝐹:𝑋–1-1→𝑊 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
43 | 41, 42 | sylan 487 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
44 | 43 | 3impb 1252 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
45 | 35, 39, 44 | 3bitr2d 295 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦)) |
46 | 45 | biimpd 218 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) |
47 | 27 | 3ad2antr1 1219 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (◡𝐹‘𝑥) ∈ ℝ) |
48 | 37 | 3ad2antr2 1220 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (◡𝐹‘𝑦) ∈ ℝ) |
49 | 26 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ 𝑋) → (◡𝐹‘𝑧) ∈ ℝ) |
50 | 49 | 3ad2antr3 1221 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (◡𝐹‘𝑧) ∈ ℝ) |
51 | | letr 10010 |
. . . . 5
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ (◡𝐹‘𝑦) ∈ ℝ ∧ (◡𝐹‘𝑧) ∈ ℝ) → (((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧)) → (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
52 | 47, 48, 50, 51 | syl3anc 1318 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧)) → (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
53 | 32 | 3adant3r3 1268 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 ≤ 𝑦 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦))) |
54 | 1, 9, 10, 7, 5 | znleval2 19723 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦 ≤ 𝑧 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧))) |
55 | 54 | 3adant3r1 1266 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 ≤ 𝑧 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧))) |
56 | 53, 55 | anbi12d 743 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧)))) |
57 | 1, 9, 10, 7, 5 | znleval2 19723 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥 ≤ 𝑧 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
58 | 57 | 3adant3r2 1267 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 ≤ 𝑧 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
59 | 52, 56, 58 | 3imtr4d 282 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) |
60 | 4, 6, 8, 31, 46, 59 | isposd 16778 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
Poset) |
61 | 36, 38 | letrid 10068 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∨ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥))) |
62 | 32, 34 | orbi12d 742 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∨ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥)))) |
63 | 61, 62 | mpbird 246 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) |
64 | 63 | 3expb 1258 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) |
65 | 64 | ralrimivva 2954 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) |
66 | 5, 7 | istos 16858 |
. 2
⊢ (𝑌 ∈ Toset ↔ (𝑌 ∈ Poset ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))) |
67 | 60, 65, 66 | sylanbrc 695 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
Toset) |