| 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 21573 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) | 
| 6 |  | relco 6125 | . . . . . . . 8
⊢ Rel
((𝐹 ∘ ≤ ) ∘
◡𝐹) | 
| 7 |  | relssdmrn 6287 | . . . . . . . 8
⊢ (Rel
((𝐹 ∘ ≤ ) ∘
◡𝐹) → ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹))) | 
| 8 | 6, 7 | ax-mp 5 | . . . . . . 7
⊢ ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) | 
| 9 |  | dmcoss 5984 | . . . . . . . . 9
⊢ dom
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ dom ◡𝐹 | 
| 10 |  | df-rn 5695 | . . . . . . . . . 10
⊢ ran 𝐹 = dom ◡𝐹 | 
| 11 |  | znleval.x | . . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝑌) | 
| 12 | 1, 11, 2, 3 | znf1o 21571 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝑋) | 
| 13 |  | f1ofo 6854 | . . . . . . . . . . 11
⊢ (𝐹:𝑊–1-1-onto→𝑋 → 𝐹:𝑊–onto→𝑋) | 
| 14 |  | forn 6822 | . . . . . . . . . . 11
⊢ (𝐹:𝑊–onto→𝑋 → ran 𝐹 = 𝑋) | 
| 15 | 12, 13, 14 | 3syl 18 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ran 𝐹 = 𝑋) | 
| 16 | 10, 15 | eqtr3id 2790 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ dom ◡𝐹 = 𝑋) | 
| 17 | 9, 16 | sseqtrid 4025 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ dom ((𝐹 ∘ ≤
) ∘ ◡𝐹) ⊆ 𝑋) | 
| 18 |  | rncoss 5985 | . . . . . . . . 9
⊢ ran
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ ran (𝐹 ∘ ≤ ) | 
| 19 |  | rncoss 5985 | . . . . . . . . . 10
⊢ ran
(𝐹 ∘ ≤ ) ⊆
ran 𝐹 | 
| 20 | 19, 15 | sseqtrid 4025 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ran (𝐹 ∘ ≤
) ⊆ 𝑋) | 
| 21 | 18, 20 | sstrid 3994 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ran ((𝐹 ∘ ≤
) ∘ ◡𝐹) ⊆ 𝑋) | 
| 22 |  | xpss12 5699 | . . . . . . . 8
⊢ ((dom
((𝐹 ∘ ≤ ) ∘
◡𝐹) ⊆ 𝑋 ∧ ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⊆ 𝑋) → (dom ((𝐹 ∘ ≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) ⊆ (𝑋 × 𝑋)) | 
| 23 | 17, 21, 22 | syl2anc 584 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (dom ((𝐹 ∘
≤ ) ∘ ◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) ⊆ (𝑋 × 𝑋)) | 
| 24 | 8, 23 | sstrid 3994 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝐹 ∘ ≤ )
∘ ◡𝐹) ⊆ (𝑋 × 𝑋)) | 
| 25 | 5, 24 | eqsstrd 4017 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ ≤ ⊆ (𝑋 × 𝑋)) | 
| 26 | 25 | ssbrd 5185 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 → 𝐴(𝑋 × 𝑋)𝐵)) | 
| 27 |  | brxp 5733 | . . . 4
⊢ (𝐴(𝑋 × 𝑋)𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) | 
| 28 | 26, 27 | imbitrdi 251 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))) | 
| 29 | 28 | pm4.71rd 562 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵))) | 
| 30 | 5 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) | 
| 31 | 30 | breqd 5153 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ 𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵)) | 
| 32 |  | brcog 5876 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) | 
| 33 | 32 | adantl 481 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) | 
| 34 |  | eqcom 2743 | . . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝐴) ↔ (◡𝐹‘𝐴) = 𝑥) | 
| 35 | 12 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑊–1-1-onto→𝑋) | 
| 36 |  | f1ocnv 6859 | . . . . . . . . . . 11
⊢ (𝐹:𝑊–1-1-onto→𝑋 → ◡𝐹:𝑋–1-1-onto→𝑊) | 
| 37 |  | f1ofn 6848 | . . . . . . . . . . 11
⊢ (◡𝐹:𝑋–1-1-onto→𝑊 → ◡𝐹 Fn 𝑋) | 
| 38 | 35, 36, 37 | 3syl 18 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ◡𝐹 Fn 𝑋) | 
| 39 |  | simprl 770 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋) | 
| 40 |  | fnbrfvb 6958 | . . . . . . . . . 10
⊢ ((◡𝐹 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((◡𝐹‘𝐴) = 𝑥 ↔ 𝐴◡𝐹𝑥)) | 
| 41 | 38, 39, 40 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴) = 𝑥 ↔ 𝐴◡𝐹𝑥)) | 
| 42 | 34, 41 | bitr2id 284 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴◡𝐹𝑥 ↔ 𝑥 = (◡𝐹‘𝐴))) | 
| 43 | 42 | anbi1d 631 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) | 
| 44 | 43 | exbidv 1920 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝐴◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ ∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) | 
| 45 | 33, 44 | bitrd 279 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ◡𝐹)𝐵 ↔ ∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵))) | 
| 46 |  | fvex 6918 | . . . . . . 7
⊢ (◡𝐹‘𝐴) ∈ V | 
| 47 |  | breq1 5145 | . . . . . . 7
⊢ (𝑥 = (◡𝐹‘𝐴) → (𝑥(𝐹 ∘ ≤ )𝐵 ↔ (◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵)) | 
| 48 | 46, 47 | ceqsexv 3531 | . . . . . 6
⊢
(∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵) | 
| 49 |  | simprr 772 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋) | 
| 50 |  | brcog 5876 | . . . . . . . 8
⊢ (((◡𝐹‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑋) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) | 
| 51 | 46, 49, 50 | sylancr 587 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) | 
| 52 |  | fvex 6918 | . . . . . . . . 9
⊢ (◡𝐹‘𝐵) ∈ V | 
| 53 |  | breq2 5146 | . . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝐵) → ((◡𝐹‘𝐴) ≤ 𝑥 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) | 
| 54 | 52, 53 | ceqsexv 3531 | . . . . . . . 8
⊢
(∃𝑥(𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)) | 
| 55 |  | eqcom 2743 | . . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹‘𝐵) ↔ (◡𝐹‘𝐵) = 𝑥) | 
| 56 |  | fnbrfvb 6958 | . . . . . . . . . . . . . 14
⊢ ((◡𝐹 Fn 𝑋 ∧ 𝐵 ∈ 𝑋) → ((◡𝐹‘𝐵) = 𝑥 ↔ 𝐵◡𝐹𝑥)) | 
| 57 | 38, 49, 56 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐵) = 𝑥 ↔ 𝐵◡𝐹𝑥)) | 
| 58 | 55, 57 | bitrid 283 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (◡𝐹‘𝐵) ↔ 𝐵◡𝐹𝑥)) | 
| 59 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 60 |  | brcnvg 5889 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝐵◡𝐹𝑥 ↔ 𝑥𝐹𝐵)) | 
| 61 | 49, 59, 60 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵◡𝐹𝑥 ↔ 𝑥𝐹𝐵)) | 
| 62 | 58, 61 | bitrd 279 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (◡𝐹‘𝐵) ↔ 𝑥𝐹𝐵)) | 
| 63 | 62 | anbi1d 631 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ (𝑥𝐹𝐵 ∧ (◡𝐹‘𝐴) ≤ 𝑥))) | 
| 64 | 63 | biancomd 463 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ ((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) | 
| 65 | 64 | exbidv 1920 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (◡𝐹‘𝐵) ∧ (◡𝐹‘𝐴) ≤ 𝑥) ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) | 
| 66 | 54, 65 | bitr3id 285 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵) ↔ ∃𝑥((◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵))) | 
| 67 | 51, 66 | bitr4d 282 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) | 
| 68 | 48, 67 | bitrid 283 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) | 
| 69 | 31, 45, 68 | 3bitrd 305 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) | 
| 70 | 69 | pm5.32da 579 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) | 
| 71 |  | df-3an 1088 | . . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) | 
| 72 | 70, 71 | bitr4di 289 | . 2
⊢ (𝑁 ∈ ℕ0
→ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) | 
| 73 | 29, 72 | bitrd 279 | 1
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) |