Proof of Theorem iseqf1olemkle
Step | Hyp | Ref
| Expression |
1 | | iseqf1olemkle.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) |
2 | | elfzelz 9970 |
. . . . . 6
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
4 | 3 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 < (◡𝐽‘𝐾)) → 𝐾 ∈ ℤ) |
5 | 4 | zred 9323 |
. . 3
⊢ ((𝜑 ∧ 𝐾 < (◡𝐽‘𝐾)) → 𝐾 ∈ ℝ) |
6 | | iseqf1olemkle.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
7 | | f1ocnv 5453 |
. . . . . . . . 9
⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
8 | 6, 7 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
9 | | f1of 5440 |
. . . . . . . 8
⊢ (◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
10 | 8, 9 | syl 14 |
. . . . . . 7
⊢ (𝜑 → ◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
11 | 10, 1 | ffvelrnd 5630 |
. . . . . 6
⊢ (𝜑 → (◡𝐽‘𝐾) ∈ (𝑀...𝑁)) |
12 | | elfzelz 9970 |
. . . . . 6
⊢ ((◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (◡𝐽‘𝐾) ∈ ℤ) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ (𝜑 → (◡𝐽‘𝐾) ∈ ℤ) |
14 | 13 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 < (◡𝐽‘𝐾)) → (◡𝐽‘𝐾) ∈ ℤ) |
15 | 14 | zred 9323 |
. . 3
⊢ ((𝜑 ∧ 𝐾 < (◡𝐽‘𝐾)) → (◡𝐽‘𝐾) ∈ ℝ) |
16 | | simpr 109 |
. . 3
⊢ ((𝜑 ∧ 𝐾 < (◡𝐽‘𝐾)) → 𝐾 < (◡𝐽‘𝐾)) |
17 | 5, 15, 16 | ltled 8027 |
. 2
⊢ ((𝜑 ∧ 𝐾 < (◡𝐽‘𝐾)) → 𝐾 ≤ (◡𝐽‘𝐾)) |
18 | 3 | zred 9323 |
. . 3
⊢ (𝜑 → 𝐾 ∈ ℝ) |
19 | | eqle 8000 |
. . 3
⊢ ((𝐾 ∈ ℝ ∧ 𝐾 = (◡𝐽‘𝐾)) → 𝐾 ≤ (◡𝐽‘𝐾)) |
20 | 18, 19 | sylan 281 |
. 2
⊢ ((𝜑 ∧ 𝐾 = (◡𝐽‘𝐾)) → 𝐾 ≤ (◡𝐽‘𝐾)) |
21 | 6 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
22 | 1 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → 𝐾 ∈ (𝑀...𝑁)) |
23 | | f1ocnvfv2 5755 |
. . . . 5
⊢ ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽‘(◡𝐽‘𝐾)) = 𝐾) |
24 | 21, 22, 23 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → (𝐽‘(◡𝐽‘𝐾)) = 𝐾) |
25 | | fveq2 5494 |
. . . . . 6
⊢ (𝑥 = (◡𝐽‘𝐾) → (𝐽‘𝑥) = (𝐽‘(◡𝐽‘𝐾))) |
26 | | id 19 |
. . . . . 6
⊢ (𝑥 = (◡𝐽‘𝐾) → 𝑥 = (◡𝐽‘𝐾)) |
27 | 25, 26 | eqeq12d 2185 |
. . . . 5
⊢ (𝑥 = (◡𝐽‘𝐾) → ((𝐽‘𝑥) = 𝑥 ↔ (𝐽‘(◡𝐽‘𝐾)) = (◡𝐽‘𝐾))) |
28 | | iseqf1olemkle.const |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) |
29 | 28 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) |
30 | | elfzuz 9966 |
. . . . . . . 8
⊢ ((◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (◡𝐽‘𝐾) ∈ (ℤ≥‘𝑀)) |
31 | 11, 30 | syl 14 |
. . . . . . 7
⊢ (𝜑 → (◡𝐽‘𝐾) ∈ (ℤ≥‘𝑀)) |
32 | 31 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → (◡𝐽‘𝐾) ∈ (ℤ≥‘𝑀)) |
33 | 3 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → 𝐾 ∈ ℤ) |
34 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → (◡𝐽‘𝐾) < 𝐾) |
35 | | elfzo2 10095 |
. . . . . 6
⊢ ((◡𝐽‘𝐾) ∈ (𝑀..^𝐾) ↔ ((◡𝐽‘𝐾) ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ ∧ (◡𝐽‘𝐾) < 𝐾)) |
36 | 32, 33, 34, 35 | syl3anbrc 1176 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → (◡𝐽‘𝐾) ∈ (𝑀..^𝐾)) |
37 | 27, 29, 36 | rspcdva 2839 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → (𝐽‘(◡𝐽‘𝐾)) = (◡𝐽‘𝐾)) |
38 | 24, 37 | eqtr3d 2205 |
. . 3
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → 𝐾 = (◡𝐽‘𝐾)) |
39 | 38, 20 | syldan 280 |
. 2
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝐾) → 𝐾 ≤ (◡𝐽‘𝐾)) |
40 | | ztri3or 9244 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ (◡𝐽‘𝐾) ∈ ℤ) → (𝐾 < (◡𝐽‘𝐾) ∨ 𝐾 = (◡𝐽‘𝐾) ∨ (◡𝐽‘𝐾) < 𝐾)) |
41 | 3, 13, 40 | syl2anc 409 |
. 2
⊢ (𝜑 → (𝐾 < (◡𝐽‘𝐾) ∨ 𝐾 = (◡𝐽‘𝐾) ∨ (◡𝐽‘𝐾) < 𝐾)) |
42 | 17, 20, 39, 41 | mpjao3dan 1302 |
1
⊢ (𝜑 → 𝐾 ≤ (◡𝐽‘𝐾)) |