| Step | Hyp | Ref
| Expression |
| 1 | | znle2.y |
. . . . 5
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
| 2 | 1 | fvexi 6920 |
. . . 4
⊢ 𝑌 ∈ V |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
V) |
| 4 | | znleval.x |
. . . 4
⊢ 𝑋 = (Base‘𝑌) |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝑋 =
(Base‘𝑌)) |
| 6 | | znle2.l |
. . . 4
⊢ ≤ =
(le‘𝑌) |
| 7 | 6 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ≤ = (le‘𝑌)) |
| 8 | | znle2.f |
. . . . . . . . . 10
⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) |
| 9 | | znle2.w |
. . . . . . . . . 10
⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) |
| 10 | 1, 4, 8, 9 | znf1o 21570 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝑋) |
| 11 | | f1ocnv 6860 |
. . . . . . . . 9
⊢ (𝐹:𝑊–1-1-onto→𝑋 → ◡𝐹:𝑋–1-1-onto→𝑊) |
| 12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋–1-1-onto→𝑊) |
| 13 | | f1of 6848 |
. . . . . . . 8
⊢ (◡𝐹:𝑋–1-1-onto→𝑊 → ◡𝐹:𝑋⟶𝑊) |
| 14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋⟶𝑊) |
| 15 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (ℤ
= if(𝑁 = 0, ℤ,
(0..^𝑁)) → (ℤ
⊆ ℤ ↔ if(𝑁
= 0, ℤ, (0..^𝑁))
⊆ ℤ)) |
| 16 | | sseq1 4009 |
. . . . . . . . . 10
⊢
((0..^𝑁) = if(𝑁 = 0, ℤ, (0..^𝑁)) → ((0..^𝑁) ⊆ ℤ ↔
if(𝑁 = 0, ℤ,
(0..^𝑁)) ⊆
ℤ)) |
| 17 | | ssid 4006 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℤ |
| 18 | | fzossz 13719 |
. . . . . . . . . 10
⊢
(0..^𝑁) ⊆
ℤ |
| 19 | 15, 16, 17, 18 | keephyp 4597 |
. . . . . . . . 9
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆
ℤ |
| 20 | 9, 19 | eqsstri 4030 |
. . . . . . . 8
⊢ 𝑊 ⊆
ℤ |
| 21 | | zssre 12620 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
| 22 | 20, 21 | sstri 3993 |
. . . . . . 7
⊢ 𝑊 ⊆
ℝ |
| 23 | | fss 6752 |
. . . . . . 7
⊢ ((◡𝐹:𝑋⟶𝑊 ∧ 𝑊 ⊆ ℝ) → ◡𝐹:𝑋⟶ℝ) |
| 24 | 14, 22, 23 | sylancl 586 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋⟶ℝ) |
| 25 | 24 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (◡𝐹‘𝑥) ∈ ℝ) |
| 26 | 25 | leidd 11829 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑥)) |
| 27 | 1, 8, 9, 6, 4 | znleval2 21574 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥 ≤ 𝑥 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑥))) |
| 28 | 27 | 3anidm23 1423 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (𝑥 ≤ 𝑥 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑥))) |
| 29 | 26, 28 | mpbird 257 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → 𝑥 ≤ 𝑥) |
| 30 | 1, 8, 9, 6, 4 | znleval2 21574 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ≤ 𝑦 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦))) |
| 31 | 1, 8, 9, 6, 4 | znleval2 21574 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑦 ≤ 𝑥 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥))) |
| 32 | 31 | 3com23 1127 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑦 ≤ 𝑥 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥))) |
| 33 | 30, 32 | anbi12d 632 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥)))) |
| 34 | 25 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (◡𝐹‘𝑥) ∈ ℝ) |
| 35 | 24 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑦 ∈ 𝑋) → (◡𝐹‘𝑦) ∈ ℝ) |
| 36 | 35 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (◡𝐹‘𝑦) ∈ ℝ) |
| 37 | 34, 36 | letri3d 11403 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥)))) |
| 38 | | f1of1 6847 |
. . . . . . . 8
⊢ (◡𝐹:𝑋–1-1-onto→𝑊 → ◡𝐹:𝑋–1-1→𝑊) |
| 39 | 12, 38 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ◡𝐹:𝑋–1-1→𝑊) |
| 40 | | f1fveq 7282 |
. . . . . . 7
⊢ ((◡𝐹:𝑋–1-1→𝑊 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
| 41 | 39, 40 | sylan 580 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
| 42 | 41 | 3impb 1115 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((◡𝐹‘𝑥) = (◡𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
| 43 | 33, 37, 42 | 3bitr2d 307 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦)) |
| 44 | 43 | biimpd 229 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) |
| 45 | 25 | 3ad2antr1 1189 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (◡𝐹‘𝑥) ∈ ℝ) |
| 46 | 35 | 3ad2antr2 1190 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (◡𝐹‘𝑦) ∈ ℝ) |
| 47 | 24 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ 𝑋) → (◡𝐹‘𝑧) ∈ ℝ) |
| 48 | 47 | 3ad2antr3 1191 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (◡𝐹‘𝑧) ∈ ℝ) |
| 49 | | letr 11355 |
. . . . 5
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ (◡𝐹‘𝑦) ∈ ℝ ∧ (◡𝐹‘𝑧) ∈ ℝ) → (((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧)) → (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
| 50 | 45, 46, 48, 49 | syl3anc 1373 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧)) → (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
| 51 | 30 | 3adant3r3 1185 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 ≤ 𝑦 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦))) |
| 52 | 1, 8, 9, 6, 4 | znleval2 21574 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦 ≤ 𝑧 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧))) |
| 53 | 52 | 3adant3r1 1183 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 ≤ 𝑧 ↔ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧))) |
| 54 | 51, 53 | anbi12d 632 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∧ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑧)))) |
| 55 | 1, 8, 9, 6, 4 | znleval2 21574 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥 ≤ 𝑧 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
| 56 | 55 | 3adant3r2 1184 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 ≤ 𝑧 ↔ (◡𝐹‘𝑥) ≤ (◡𝐹‘𝑧))) |
| 57 | 50, 54, 56 | 3imtr4d 294 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) |
| 58 | 3, 5, 7, 29, 44, 57 | isposd 18368 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
Poset) |
| 59 | 34, 36 | letrid 11413 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∨ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥))) |
| 60 | 30, 32 | orbi12d 919 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) ↔ ((◡𝐹‘𝑥) ≤ (◡𝐹‘𝑦) ∨ (◡𝐹‘𝑦) ≤ (◡𝐹‘𝑥)))) |
| 61 | 59, 60 | mpbird 257 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) |
| 62 | 61 | 3expb 1121 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) |
| 63 | 62 | ralrimivva 3202 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) |
| 64 | 4, 6 | istos 18463 |
. 2
⊢ (𝑌 ∈ Toset ↔ (𝑌 ∈ Poset ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))) |
| 65 | 58, 63, 64 | sylanbrc 583 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
Toset) |