Step | Hyp | Ref
| Expression |
1 | | fveqeq2 6783 |
. . . . . 6
⊢ (𝑎 = ran 𝑧 → ((♯‘𝑎) = 𝐾 ↔ (♯‘ran 𝑧) = 𝐾)) |
2 | | fzfid 13693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (1...𝑁) ∈ Fin) |
3 | | eleq1w 2821 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑧 → (𝑓 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
4 | | feq1 6581 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑧 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑧:(1...𝐾)⟶(1...𝑁))) |
5 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑧 → (𝑓‘𝑥) = (𝑧‘𝑥)) |
6 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑧 → (𝑓‘𝑦) = (𝑧‘𝑦)) |
7 | 5, 6 | breq12d 5087 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑧 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑧‘𝑥) < (𝑧‘𝑦))) |
8 | 7 | imbi2d 341 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑧 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)))) |
9 | 8 | ralbidv 3112 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑧 → (∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)))) |
10 | 9 | ralbidv 3112 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑧 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)))) |
11 | 4, 10 | anbi12d 631 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑧 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑧:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦))))) |
12 | 3, 11 | bibi12d 346 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑧 → ((𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) ↔ (𝑧 ∈ 𝐴 ↔ (𝑧:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)))))) |
13 | | sticksstones2.4 |
. . . . . . . . . . . . . 14
⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} |
14 | | abeq2 2872 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))) |
15 | 13, 14 | mpbi 229 |
. . . . . . . . . . . . 13
⊢
∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) |
16 | 15 | spi 2177 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) |
17 | 12, 16 | chvarvv 2002 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐴 ↔ (𝑧:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)))) |
18 | 17 | biimpi 215 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐴 → (𝑧:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)))) |
19 | 18 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)))) |
20 | 19 | simpld 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧:(1...𝐾)⟶(1...𝑁)) |
21 | 20 | frnd 6608 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ran 𝑧 ⊆ (1...𝑁)) |
22 | 2, 21 | sselpwd 5250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ran 𝑧 ∈ 𝒫 (1...𝑁)) |
23 | 20 | ffnd 6601 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 Fn (1...𝐾)) |
24 | | hashfn 14090 |
. . . . . . . . . . 11
⊢ (𝑧 Fn (1...𝐾) → (♯‘𝑧) = (♯‘(1...𝐾))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (♯‘𝑧) = (♯‘(1...𝐾))) |
26 | | sticksstones2.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
27 | 26 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐾 ∈
ℕ0) |
28 | | hashfz1 14060 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ (♯‘(1...𝐾)) = 𝐾) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (♯‘(1...𝐾)) = 𝐾) |
30 | 25, 29 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (♯‘𝑧) = 𝐾) |
31 | 30 | eqcomd 2744 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐾 = (♯‘𝑧)) |
32 | | fzfid 13693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (1...𝐾) ∈ Fin) |
33 | | elfznn 13285 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (1...𝐾) → 𝑎 ∈ ℕ) |
34 | 33 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) → 𝑎 ∈ ℕ) |
35 | 34 | nnred 11988 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) → 𝑎 ∈ ℝ) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → 𝑎 ∈ ℝ) |
37 | | elfznn 13285 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ (1...𝐾) → 𝑏 ∈ ℕ) |
38 | 37 | nnred 11988 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ (1...𝐾) → 𝑏 ∈ ℝ) |
39 | 38 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → 𝑏 ∈ ℝ) |
40 | | lttri2 11057 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 ≠ 𝑏 ↔ (𝑎 < 𝑏 ∨ 𝑏 < 𝑎))) |
41 | 36, 39, 40 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑎 ≠ 𝑏 ↔ (𝑎 < 𝑏 ∨ 𝑏 < 𝑎))) |
42 | 20 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) → 𝑧:(1...𝐾)⟶(1...𝑁)) |
43 | | simp3 1137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) → 𝑎 ∈ (1...𝐾)) |
44 | 42, 43 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) → (𝑧‘𝑎) ∈ (1...𝑁)) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑧‘𝑎) ∈ (1...𝑁)) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑎 < 𝑏) → (𝑧‘𝑎) ∈ (1...𝑁)) |
47 | | elfznn 13285 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧‘𝑎) ∈ (1...𝑁) → (𝑧‘𝑎) ∈ ℕ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑎 < 𝑏) → (𝑧‘𝑎) ∈ ℕ) |
49 | 48 | nnred 11988 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑎 < 𝑏) → (𝑧‘𝑎) ∈ ℝ) |
50 | 19 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦))) |
51 | 50 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦))) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦))) |
53 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → 𝑎 ∈ (1...𝐾)) |
54 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → 𝑏 ∈ (1...𝐾)) |
55 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑎 → (𝑥 < 𝑦 ↔ 𝑎 < 𝑦)) |
56 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑎 → (𝑧‘𝑥) = (𝑧‘𝑎)) |
57 | 56 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑎 → ((𝑧‘𝑥) < (𝑧‘𝑦) ↔ (𝑧‘𝑎) < (𝑧‘𝑦))) |
58 | 55, 57 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑎 → ((𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)) ↔ (𝑎 < 𝑦 → (𝑧‘𝑎) < (𝑧‘𝑦)))) |
59 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑏 → (𝑎 < 𝑦 ↔ 𝑎 < 𝑏)) |
60 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑏 → (𝑧‘𝑦) = (𝑧‘𝑏)) |
61 | 60 | breq2d 5086 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑏 → ((𝑧‘𝑎) < (𝑧‘𝑦) ↔ (𝑧‘𝑎) < (𝑧‘𝑏))) |
62 | 59, 61 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑏 → ((𝑎 < 𝑦 → (𝑧‘𝑎) < (𝑧‘𝑦)) ↔ (𝑎 < 𝑏 → (𝑧‘𝑎) < (𝑧‘𝑏)))) |
63 | 58, 62 | rspc2v 3570 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ (1...𝐾) ∧ 𝑏 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)) → (𝑎 < 𝑏 → (𝑧‘𝑎) < (𝑧‘𝑏)))) |
64 | 53, 54, 63 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)) → (𝑎 < 𝑏 → (𝑧‘𝑎) < (𝑧‘𝑏)))) |
65 | 52, 64 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑎 < 𝑏 → (𝑧‘𝑎) < (𝑧‘𝑏))) |
66 | 65 | imp 407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑎 < 𝑏) → (𝑧‘𝑎) < (𝑧‘𝑏)) |
67 | 49, 66 | ltned 11111 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑎 < 𝑏) → (𝑧‘𝑎) ≠ (𝑧‘𝑏)) |
68 | 42 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑧‘𝑏) ∈ (1...𝑁)) |
69 | | elfznn 13285 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧‘𝑏) ∈ (1...𝑁) → (𝑧‘𝑏) ∈ ℕ) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑧‘𝑏) ∈ ℕ) |
71 | 70 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑧‘𝑏) ∈ ℝ) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑏 < 𝑎) → (𝑧‘𝑏) ∈ ℝ) |
73 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑏 → (𝑥 < 𝑦 ↔ 𝑏 < 𝑦)) |
74 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑏 → (𝑧‘𝑥) = (𝑧‘𝑏)) |
75 | 74 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑏 → ((𝑧‘𝑥) < (𝑧‘𝑦) ↔ (𝑧‘𝑏) < (𝑧‘𝑦))) |
76 | 73, 75 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑏 → ((𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)) ↔ (𝑏 < 𝑦 → (𝑧‘𝑏) < (𝑧‘𝑦)))) |
77 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑎 → (𝑏 < 𝑦 ↔ 𝑏 < 𝑎)) |
78 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑎 → (𝑧‘𝑦) = (𝑧‘𝑎)) |
79 | 78 | breq2d 5086 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑎 → ((𝑧‘𝑏) < (𝑧‘𝑦) ↔ (𝑧‘𝑏) < (𝑧‘𝑎))) |
80 | 77, 79 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑎 → ((𝑏 < 𝑦 → (𝑧‘𝑏) < (𝑧‘𝑦)) ↔ (𝑏 < 𝑎 → (𝑧‘𝑏) < (𝑧‘𝑎)))) |
81 | 76, 80 | rspc2v 3570 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 ∈ (1...𝐾) ∧ 𝑎 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)) → (𝑏 < 𝑎 → (𝑧‘𝑏) < (𝑧‘𝑎)))) |
82 | 54, 53, 81 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑧‘𝑥) < (𝑧‘𝑦)) → (𝑏 < 𝑎 → (𝑧‘𝑏) < (𝑧‘𝑎)))) |
83 | 52, 82 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑏 < 𝑎 → (𝑧‘𝑏) < (𝑧‘𝑎))) |
84 | 83 | imp 407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑏 < 𝑎) → (𝑧‘𝑏) < (𝑧‘𝑎)) |
85 | 72, 84 | ltned 11111 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑏 < 𝑎) → (𝑧‘𝑏) ≠ (𝑧‘𝑎)) |
86 | 85 | necomd 2999 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ 𝑏 < 𝑎) → (𝑧‘𝑎) ≠ (𝑧‘𝑏)) |
87 | 67, 86 | jaodan 955 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) ∧ (𝑎 < 𝑏 ∨ 𝑏 < 𝑎)) → (𝑧‘𝑎) ≠ (𝑧‘𝑏)) |
88 | 87 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → ((𝑎 < 𝑏 ∨ 𝑏 < 𝑎) → (𝑧‘𝑎) ≠ (𝑧‘𝑏))) |
89 | 41, 88 | sylbid 239 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → (𝑎 ≠ 𝑏 → (𝑧‘𝑎) ≠ (𝑧‘𝑏))) |
90 | 89 | necon4d 2967 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) ∧ 𝑏 ∈ (1...𝐾)) → ((𝑧‘𝑎) = (𝑧‘𝑏) → 𝑎 = 𝑏)) |
91 | 90 | ralrimiva 3103 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ (1...𝐾)) → ∀𝑏 ∈ (1...𝐾)((𝑧‘𝑎) = (𝑧‘𝑏) → 𝑎 = 𝑏)) |
92 | 91 | 3expa 1117 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑎 ∈ (1...𝐾)) → ∀𝑏 ∈ (1...𝐾)((𝑧‘𝑎) = (𝑧‘𝑏) → 𝑎 = 𝑏)) |
93 | 92 | ralrimiva 3103 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑎 ∈ (1...𝐾)∀𝑏 ∈ (1...𝐾)((𝑧‘𝑎) = (𝑧‘𝑏) → 𝑎 = 𝑏)) |
94 | 20, 93 | jca 512 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑎 ∈ (1...𝐾)∀𝑏 ∈ (1...𝐾)((𝑧‘𝑎) = (𝑧‘𝑏) → 𝑎 = 𝑏))) |
95 | | dff13 7128 |
. . . . . . . . . 10
⊢ (𝑧:(1...𝐾)–1-1→(1...𝑁) ↔ (𝑧:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑎 ∈ (1...𝐾)∀𝑏 ∈ (1...𝐾)((𝑧‘𝑎) = (𝑧‘𝑏) → 𝑎 = 𝑏))) |
96 | 94, 95 | sylibr 233 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧:(1...𝐾)–1-1→(1...𝑁)) |
97 | | hashf1rn 14067 |
. . . . . . . . 9
⊢
(((1...𝐾) ∈ Fin
∧ 𝑧:(1...𝐾)–1-1→(1...𝑁)) → (♯‘𝑧) = (♯‘ran 𝑧)) |
98 | 32, 96, 97 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (♯‘𝑧) = (♯‘ran 𝑧)) |
99 | 31, 98 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐾 = (♯‘ran 𝑧)) |
100 | 99 | eqcomd 2744 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (♯‘ran 𝑧) = 𝐾) |
101 | 1, 22, 100 | elrabd 3626 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ran 𝑧 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) |
102 | | sticksstones2.3 |
. . . . . . 7
⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} |
103 | 102 | eleq2i 2830 |
. . . . . 6
⊢ (ran
𝑧 ∈ 𝐵 ↔ ran 𝑧 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) |
104 | 103 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (ran 𝑧 ∈ 𝐵 ↔ ran 𝑧 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾})) |
105 | 101, 104 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ran 𝑧 ∈ 𝐵) |
106 | | sticksstones2.5 |
. . . 4
⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧) |
107 | 105, 106 | fmptd 6988 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
108 | | sticksstones2.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
109 | 108 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → 𝑁 ∈
ℕ0) |
110 | 109 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → 𝑁 ∈
ℕ0) |
111 | 26 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → 𝐾 ∈
ℕ0) |
112 | 111 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → 𝐾 ∈
ℕ0) |
113 | | simpl2 1191 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ 𝐴) |
114 | | simpl3 1192 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ 𝐴) |
115 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → 𝑖 ≠ 𝑗) |
116 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑠 → (𝑖‘𝑟) = (𝑖‘𝑠)) |
117 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑠 → (𝑗‘𝑟) = (𝑗‘𝑠)) |
118 | 116, 117 | neeq12d 3005 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑠 → ((𝑖‘𝑟) ≠ (𝑗‘𝑟) ↔ (𝑖‘𝑠) ≠ (𝑗‘𝑠))) |
119 | 118 | cbvrabv 3426 |
. . . . . . . . . . 11
⊢ {𝑟 ∈ (1...𝐾) ∣ (𝑖‘𝑟) ≠ (𝑗‘𝑟)} = {𝑠 ∈ (1...𝐾) ∣ (𝑖‘𝑠) ≠ (𝑗‘𝑠)} |
120 | 119 | infeq1i 9237 |
. . . . . . . . . 10
⊢
inf({𝑟 ∈
(1...𝐾) ∣ (𝑖‘𝑟) ≠ (𝑗‘𝑟)}, ℝ, < ) = inf({𝑠 ∈ (1...𝐾) ∣ (𝑖‘𝑠) ≠ (𝑗‘𝑠)}, ℝ, < ) |
121 | 110, 112,
13, 113, 114, 115, 120 | sticksstones1 40102 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → ran 𝑖 ≠ ran 𝑗) |
122 | 106 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧)) |
123 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) ∧ 𝑧 = 𝑖) → 𝑧 = 𝑖) |
124 | 123 | rneqd 5847 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) ∧ 𝑧 = 𝑖) → ran 𝑧 = ran 𝑖) |
125 | | fzfid 13693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → (1...𝑁) ∈ Fin) |
126 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑖 → (𝑓 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴)) |
127 | | feq1 6581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑖 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑖:(1...𝐾)⟶(1...𝑁))) |
128 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑖 → (𝑓‘𝑥) = (𝑖‘𝑥)) |
129 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑖 → (𝑓‘𝑦) = (𝑖‘𝑦)) |
130 | 128, 129 | breq12d 5087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑖 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑖‘𝑥) < (𝑖‘𝑦))) |
131 | 130 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑖 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑖‘𝑥) < (𝑖‘𝑦)))) |
132 | 131 | 2ralbidv 3129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑖 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑖‘𝑥) < (𝑖‘𝑦)))) |
133 | 127, 132 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑖 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑖:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑖‘𝑥) < (𝑖‘𝑦))))) |
134 | 126, 133 | bibi12d 346 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑖 → ((𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) ↔ (𝑖 ∈ 𝐴 ↔ (𝑖:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑖‘𝑥) < (𝑖‘𝑦)))))) |
135 | 134, 16 | chvarvv 2002 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ 𝐴 ↔ (𝑖:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑖‘𝑥) < (𝑖‘𝑦)))) |
136 | 135 | biimpi 215 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ 𝐴 → (𝑖:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑖‘𝑥) < (𝑖‘𝑦)))) |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑖:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑖‘𝑥) < (𝑖‘𝑦)))) |
138 | 137 | simpld 495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑖:(1...𝐾)⟶(1...𝑁)) |
139 | 138 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → 𝑖:(1...𝐾)⟶(1...𝑁)) |
140 | 139 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → 𝑖:(1...𝐾)⟶(1...𝑁)) |
141 | 140 | frnd 6608 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → ran 𝑖 ⊆ (1...𝑁)) |
142 | 125, 141 | sselpwd 5250 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → ran 𝑖 ∈ 𝒫 (1...𝑁)) |
143 | 122, 124,
113, 142 | fvmptd 6882 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → (𝐹‘𝑖) = ran 𝑖) |
144 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) ∧ 𝑧 = 𝑗) → 𝑧 = 𝑗) |
145 | 144 | rneqd 5847 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) ∧ 𝑧 = 𝑗) → ran 𝑧 = ran 𝑗) |
146 | | fzfid 13693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
147 | 146 | 3ad2ant1 1132 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → (1...𝑁) ∈ Fin) |
148 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑗 → (𝑓 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴)) |
149 | | feq1 6581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑗 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑗:(1...𝐾)⟶(1...𝑁))) |
150 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑗 → (𝑓‘𝑥) = (𝑗‘𝑥)) |
151 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑗 → (𝑓‘𝑦) = (𝑗‘𝑦)) |
152 | 150, 151 | breq12d 5087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑗 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑗‘𝑥) < (𝑗‘𝑦))) |
153 | 152 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑗 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑗‘𝑥) < (𝑗‘𝑦)))) |
154 | 153 | 2ralbidv 3129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑗 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑗‘𝑥) < (𝑗‘𝑦)))) |
155 | 149, 154 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑗 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑗:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑗‘𝑥) < (𝑗‘𝑦))))) |
156 | 148, 155 | bibi12d 346 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑗 → ((𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) ↔ (𝑗 ∈ 𝐴 ↔ (𝑗:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑗‘𝑥) < (𝑗‘𝑦)))))) |
157 | 156, 16 | chvarvv 2002 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ 𝐴 ↔ (𝑗:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑗‘𝑥) < (𝑗‘𝑦)))) |
158 | 157 | biimpi 215 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 𝐴 → (𝑗:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑗‘𝑥) < (𝑗‘𝑦)))) |
159 | 158 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑗:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑗‘𝑥) < (𝑗‘𝑦)))) |
160 | 159 | simpld 495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗:(1...𝐾)⟶(1...𝑁)) |
161 | 160 | 3adant2 1130 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → 𝑗:(1...𝐾)⟶(1...𝑁)) |
162 | 161 | frnd 6608 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → ran 𝑗 ⊆ (1...𝑁)) |
163 | 147, 162 | sselpwd 5250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → ran 𝑗 ∈ 𝒫 (1...𝑁)) |
164 | 163 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → ran 𝑗 ∈ 𝒫 (1...𝑁)) |
165 | 122, 145,
114, 164 | fvmptd 6882 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → (𝐹‘𝑗) = ran 𝑗) |
166 | 121, 143,
165 | 3netr4d 3021 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) ∧ 𝑖 ≠ 𝑗) → (𝐹‘𝑖) ≠ (𝐹‘𝑗)) |
167 | 166 | ex 413 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → (𝑖 ≠ 𝑗 → (𝐹‘𝑖) ≠ (𝐹‘𝑗))) |
168 | 167 | necon4d 2967 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴) → ((𝐹‘𝑖) = (𝐹‘𝑗) → 𝑖 = 𝑗)) |
169 | 168 | 3expa 1117 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑗 ∈ 𝐴) → ((𝐹‘𝑖) = (𝐹‘𝑗) → 𝑖 = 𝑗)) |
170 | 169 | ralrimiva 3103 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑗 ∈ 𝐴 ((𝐹‘𝑖) = (𝐹‘𝑗) → 𝑖 = 𝑗)) |
171 | 170 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝐹‘𝑖) = (𝐹‘𝑗) → 𝑖 = 𝑗)) |
172 | 107, 171 | jca 512 |
. 2
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝐹‘𝑖) = (𝐹‘𝑗) → 𝑖 = 𝑗))) |
173 | | dff13 7128 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝐹‘𝑖) = (𝐹‘𝑗) → 𝑖 = 𝑗))) |
174 | 172, 173 | sylibr 233 |
1
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) |