Step | Hyp | Ref
| Expression |
1 | | znle2.y |
. . . . . . 7
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
2 | | znle2.f |
. . . . . . 7
⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) |
3 | | znle2.w |
. . . . . . 7
⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) |
4 | | znle2.l |
. . . . . . 7
⊢ ≤ =
(le‘𝑌) |
5 | 1, 2, 3, 4 | znle2 19721 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) |
6 | | relco 5550 |
. . . . . . . 8
⊢ Rel
((𝐹 ∘ ≤ ) ∘
◡𝐹) |
7 | | relssdmrn 5573 |
. . . . . . . 8
⊢ (Rel
((𝐹 ∘ ≤ ) ∘
◡𝐹) → ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) |
9 | | dmcoss 5306 |
. . . . . . . . 9
⊢ dom
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ dom ◡𝐹 |
10 | | df-rn 5049 |
. . . . . . . . . 10
⊢ ran 𝐹 = dom ◡𝐹 |
11 | | znleval.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝑌) |
12 | 1, 11, 2, 3 | znf1o 19719 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝑋) |
13 | | f1ofo 6057 |
. . . . . . . . . . 11
⊢ (𝐹:𝑊–1-1-onto→𝑋 → 𝐹:𝑊–onto→𝑋) |
14 | | forn 6031 |
. . . . . . . . . . 11
⊢ (𝐹:𝑊–onto→𝑋 → ran 𝐹 = 𝑋) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ran 𝐹 = 𝑋) |
16 | 10, 15 | syl5eqr 2658 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ dom ◡𝐹 = 𝑋) |
17 | 9, 16 | syl5sseq 3616 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ dom ((𝐹 ∘ ≤
) ∘ ◡𝐹) ⊆ 𝑋) |
18 | | rncoss 5307 |
. . . . . . . . 9
⊢ ran
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ ran (𝐹 ∘ ≤ ) |
19 | | rncoss 5307 |
. . . . . . . . . 10
⊢ ran
(𝐹 ∘ ≤ ) ⊆
ran 𝐹 |
20 | 19, 15 | syl5sseq 3616 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ran (𝐹 ∘ ≤
) ⊆ 𝑋) |
21 | 18, 20 | syl5ss 3579 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ran ((𝐹 ∘ ≤
) ∘ ◡𝐹) ⊆ 𝑋) |
22 | | xpss12 5148 |
. . . . . . . 8
⊢ ((dom
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ 𝑋 ∧ ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ 𝑋) → (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) ⊆ (𝑋 × 𝑋)) |
23 | 17, 21, 22 | syl2anc 691 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (dom ((𝐹 ∘
≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) ⊆ (𝑋 × 𝑋)) |
24 | 8, 23 | syl5ss 3579 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝐹 ∘ ≤ )
∘ ◡𝐹) ⊆ (𝑋 × 𝑋)) |
25 | 5, 24 | eqsstrd 3602 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ≤ ⊆ (𝑋 × 𝑋)) |
26 | 25 | ssbrd 4626 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 → 𝐴(𝑋 × 𝑋)𝐵)) |
27 | | brxp 5071 |
. . . 4
⊢ (𝐴(𝑋 × 𝑋)𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) |
28 | 26, 27 | syl6ib 240 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))) |
29 | 28 | pm4.71rd 665 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵))) |
30 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) |
31 | 30 | breqd 4594 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ 𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵)) |
32 | | brcog 5210 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
33 | 32 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
34 | | eqcom 2617 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝐴) ↔ (◡𝐹‘𝐴) = 𝑥) |
35 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑊–1-1-onto→𝑋) |
36 | | f1ocnv 6062 |
. . . . . . . . . . 11
⊢ (𝐹:𝑊–1-1-onto→𝑋 → ◡𝐹:𝑋–1-1-onto→𝑊) |
37 | | f1ofn 6051 |
. . . . . . . . . . 11
⊢ (◡𝐹:𝑋–1-1-onto→𝑊 → ◡𝐹 Fn 𝑋) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ◡𝐹 Fn 𝑋) |
39 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋) |
40 | | fnbrfvb 6146 |
. . . . . . . . . 10
⊢ ((◡𝐹 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((◡𝐹‘𝐴) = 𝑥 ↔ 𝐴◡𝐹𝑥)) |
41 | 38, 39, 40 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴) = 𝑥 ↔ 𝐴◡𝐹𝑥)) |
42 | 34, 41 | syl5rbb 272 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴◡𝐹𝑥 ↔ 𝑥 = (◡𝐹‘𝐴))) |
43 | 42 | anbi1d 737 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
44 | 43 | exbidv 1837 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ ∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
45 | 33, 44 | bitrd 267 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
46 | | fvex 6113 |
. . . . . . 7
⊢ (◡𝐹‘𝐴) ∈ V |
47 | | breq1 4586 |
. . . . . . 7
⊢ (𝑥 = (◡𝐹‘𝐴) → (𝑥(𝐹 ∘ ≤ )𝐵 ↔ (◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵)) |
48 | 46, 47 | ceqsexv 3215 |
. . . . . 6
⊢
(∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵) |
49 | | simprr 792 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋) |
50 | | brcog 5210 |
. . . . . . . 8
⊢ (((◡𝐹‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑋) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
51 | 46, 49, 50 | sylancr 694 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
52 | | fvex 6113 |
. . . . . . . . 9
⊢ (◡𝐹‘𝐵) ∈ V |
53 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝐵) → ((◡𝐹‘𝐴) ≤ 𝑥 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
54 | 52, 53 | ceqsexv 3215 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)) |
55 | | eqcom 2617 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹‘𝐵) ↔ (◡𝐹‘𝐵) = 𝑥) |
56 | | fnbrfvb 6146 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 Fn 𝑋 ∧ 𝐵 ∈ 𝑋) → ((◡𝐹‘𝐵) = 𝑥 ↔ 𝐵◡𝐹𝑥)) |
57 | 38, 49, 56 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐵) = 𝑥 ↔ 𝐵◡𝐹𝑥)) |
58 | 55, 57 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (◡𝐹‘𝐵) ↔ 𝐵◡𝐹𝑥)) |
59 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
60 | | brcnvg 5225 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝐵◡𝐹𝑥 ↔ 𝑥𝐹𝐵)) |
61 | 49, 59, 60 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵◡𝐹𝑥 ↔ 𝑥𝐹𝐵)) |
62 | 58, 61 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (◡𝐹‘𝐵) ↔ 𝑥𝐹𝐵)) |
63 | 62 | anbi1d 737 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ (𝑥𝐹𝐵 ∧ (◡𝐹‘𝐴) ≤ 𝑥))) |
64 | | ancom 465 |
. . . . . . . . . 10
⊢ (((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵) ↔ (𝑥𝐹𝐵 ∧ (◡𝐹‘𝐴) ≤ 𝑥)) |
65 | 63, 64 | syl6bbr 277 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ ((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
66 | 65 | exbidv 1837 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
67 | 54, 66 | syl5bbr 273 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵) ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
68 | 51, 67 | bitr4d 270 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
69 | 48, 68 | syl5bb 271 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
70 | 31, 45, 69 | 3bitrd 293 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
71 | 70 | pm5.32da 671 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) |
72 | | df-3an 1033 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
73 | 71, 72 | syl6bbr 277 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) |
74 | 29, 73 | bitrd 267 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) |