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 20523 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) |
6 | | relco 6113 |
. . . . . . . 8
⊢ Rel
((𝐹 ∘ ≤ ) ∘
◡𝐹) |
7 | | relssdmrn 6137 |
. . . . . . . 8
⊢ (Rel
((𝐹 ∘ ≤ ) ∘
◡𝐹) → ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) |
9 | | dmcoss 5845 |
. . . . . . . . 9
⊢ dom
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ dom ◡𝐹 |
10 | | df-rn 5567 |
. . . . . . . . . 10
⊢ ran 𝐹 = dom ◡𝐹 |
11 | | znleval.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝑌) |
12 | 1, 11, 2, 3 | znf1o 20521 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝑋) |
13 | | f1ofo 6673 |
. . . . . . . . . . 11
⊢ (𝐹:𝑊–1-1-onto→𝑋 → 𝐹:𝑊–onto→𝑋) |
14 | | forn 6641 |
. . . . . . . . . . 11
⊢ (𝐹:𝑊–onto→𝑋 → ran 𝐹 = 𝑋) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ran 𝐹 = 𝑋) |
16 | 10, 15 | eqtr3id 2792 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ dom ◡𝐹 = 𝑋) |
17 | 9, 16 | sseqtrid 3958 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ dom ((𝐹 ∘ ≤
) ∘ ◡𝐹) ⊆ 𝑋) |
18 | | rncoss 5846 |
. . . . . . . . 9
⊢ ran
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ ran (𝐹 ∘ ≤ ) |
19 | | rncoss 5846 |
. . . . . . . . . 10
⊢ ran
(𝐹 ∘ ≤ ) ⊆
ran 𝐹 |
20 | 19, 15 | sseqtrid 3958 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ran (𝐹 ∘ ≤
) ⊆ 𝑋) |
21 | 18, 20 | sstrid 3917 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ran ((𝐹 ∘ ≤
) ∘ ◡𝐹) ⊆ 𝑋) |
22 | | xpss12 5571 |
. . . . . . . 8
⊢ ((dom
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ 𝑋 ∧ ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ 𝑋) → (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) ⊆ (𝑋 × 𝑋)) |
23 | 17, 21, 22 | syl2anc 587 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (dom ((𝐹 ∘
≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) ⊆ (𝑋 × 𝑋)) |
24 | 8, 23 | sstrid 3917 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝐹 ∘ ≤ )
∘ ◡𝐹) ⊆ (𝑋 × 𝑋)) |
25 | 5, 24 | eqsstrd 3944 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ≤ ⊆ (𝑋 × 𝑋)) |
26 | 25 | ssbrd 5101 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 → 𝐴(𝑋 × 𝑋)𝐵)) |
27 | | brxp 5603 |
. . . 4
⊢ (𝐴(𝑋 × 𝑋)𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) |
28 | 26, 27 | syl6ib 254 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))) |
29 | 28 | pm4.71rd 566 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵))) |
30 | 5 | adantr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) |
31 | 30 | breqd 5069 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ 𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵)) |
32 | | brcog 5740 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
33 | 32 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
34 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝐴) ↔ (◡𝐹‘𝐴) = 𝑥) |
35 | 12 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑊–1-1-onto→𝑋) |
36 | | f1ocnv 6678 |
. . . . . . . . . . 11
⊢ (𝐹:𝑊–1-1-onto→𝑋 → ◡𝐹:𝑋–1-1-onto→𝑊) |
37 | | f1ofn 6667 |
. . . . . . . . . . 11
⊢ (◡𝐹:𝑋–1-1-onto→𝑊 → ◡𝐹 Fn 𝑋) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ◡𝐹 Fn 𝑋) |
39 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋) |
40 | | fnbrfvb 6770 |
. . . . . . . . . 10
⊢ ((◡𝐹 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((◡𝐹‘𝐴) = 𝑥 ↔ 𝐴◡𝐹𝑥)) |
41 | 38, 39, 40 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴) = 𝑥 ↔ 𝐴◡𝐹𝑥)) |
42 | 34, 41 | bitr2id 287 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴◡𝐹𝑥 ↔ 𝑥 = (◡𝐹‘𝐴))) |
43 | 42 | anbi1d 633 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
44 | 43 | exbidv 1929 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ ∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
45 | 33, 44 | bitrd 282 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) |
46 | | fvex 6735 |
. . . . . . 7
⊢ (◡𝐹‘𝐴) ∈ V |
47 | | breq1 5061 |
. . . . . . 7
⊢ (𝑥 = (◡𝐹‘𝐴) → (𝑥(𝐹 ∘ ≤ )𝐵 ↔ (◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵)) |
48 | 46, 47 | ceqsexv 3460 |
. . . . . 6
⊢
(∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵) |
49 | | simprr 773 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋) |
50 | | brcog 5740 |
. . . . . . . 8
⊢ (((◡𝐹‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑋) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
51 | 46, 49, 50 | sylancr 590 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
52 | | fvex 6735 |
. . . . . . . . 9
⊢ (◡𝐹‘𝐵) ∈ V |
53 | | breq2 5062 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝐵) → ((◡𝐹‘𝐴) ≤ 𝑥 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
54 | 52, 53 | ceqsexv 3460 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)) |
55 | | eqcom 2744 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹‘𝐵) ↔ (◡𝐹‘𝐵) = 𝑥) |
56 | | fnbrfvb 6770 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 Fn 𝑋 ∧ 𝐵 ∈ 𝑋) → ((◡𝐹‘𝐵) = 𝑥 ↔ 𝐵◡𝐹𝑥)) |
57 | 38, 49, 56 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐵) = 𝑥 ↔ 𝐵◡𝐹𝑥)) |
58 | 55, 57 | syl5bb 286 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (◡𝐹‘𝐵) ↔ 𝐵◡𝐹𝑥)) |
59 | | vex 3417 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
60 | | brcnvg 5753 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝐵◡𝐹𝑥 ↔ 𝑥𝐹𝐵)) |
61 | 49, 59, 60 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵◡𝐹𝑥 ↔ 𝑥𝐹𝐵)) |
62 | 58, 61 | bitrd 282 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (◡𝐹‘𝐵) ↔ 𝑥𝐹𝐵)) |
63 | 62 | anbi1d 633 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ (𝑥𝐹𝐵 ∧ (◡𝐹‘𝐴) ≤ 𝑥))) |
64 | 63 | biancomd 467 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ ((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
65 | 64 | exbidv 1929 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
66 | 54, 65 | bitr3id 288 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵) ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) |
67 | 51, 66 | bitr4d 285 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
68 | 48, 67 | syl5bb 286 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
69 | 31, 45, 68 | 3bitrd 308 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
70 | 69 | pm5.32da 582 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) |
71 | | df-3an 1091 |
. . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) |
72 | 70, 71 | bitr4di 292 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) |
73 | 29, 72 | bitrd 282 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) |