Step | Hyp | Ref
| Expression |
1 | | sticksstones1.7 |
. . . . . 6
⊢ 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < )) |
3 | | ltso 10938 |
. . . . . . 7
⊢ < Or
ℝ |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
5 | | fzfid 13573 |
. . . . . . . 8
⊢ (𝜑 → (1...𝐾) ∈ Fin) |
6 | | ssrab2 4008 |
. . . . . . . . 9
⊢ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾) |
7 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) |
8 | | ssfi 8874 |
. . . . . . . 8
⊢
(((1...𝐾) ∈ Fin
∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) |
9 | 5, 7, 8 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) |
10 | | sticksstones1.6 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
11 | | rabeq0 4314 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧)) |
12 | | nne 2945 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑧) = (𝑌‘𝑧)) |
13 | 12 | ralbii 3089 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
(1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) |
14 | 11, 13 | bitri 278 |
. . . . . . . . . . . 12
⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) |
15 | | feq1 6545 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁))) |
16 | | fveq1 6735 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑋 → (𝑓‘𝑥) = (𝑋‘𝑥)) |
17 | | fveq1 6735 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑋 → (𝑓‘𝑦) = (𝑋‘𝑦)) |
18 | 16, 17 | breq12d 5081 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑋 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑋‘𝑥) < (𝑋‘𝑦))) |
19 | 18 | imbi2d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))) |
20 | 19 | 2ralbidv 3121 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑋 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))) |
21 | 15, 20 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑋 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))) |
22 | | sticksstones1.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} |
23 | | abeq2 2870 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))) |
24 | 22, 23 | mpbi 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) |
25 | 24 | spi 2182 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) |
26 | 25 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ 𝐴 → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) |
27 | 26 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) |
28 | 27 | ralrimiva 3106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑓 ∈ 𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) |
29 | | sticksstones1.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
30 | 21, 28, 29 | rspcdva 3552 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))) |
31 | 30 | simpld 498 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋:(1...𝐾)⟶(1...𝑁)) |
32 | 31 | ffnd 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 Fn (1...𝐾)) |
33 | 32 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 Fn (1...𝐾)) |
34 | | sticksstones1.5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
35 | | feq1 6545 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑌 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑌:(1...𝐾)⟶(1...𝑁))) |
36 | | fveq1 6735 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑌 → (𝑓‘𝑥) = (𝑌‘𝑥)) |
37 | | fveq1 6735 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑌 → (𝑓‘𝑦) = (𝑌‘𝑦)) |
38 | 36, 37 | breq12d 5081 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑌 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑌‘𝑥) < (𝑌‘𝑦))) |
39 | 38 | imbi2d 344 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) |
40 | 39 | 2ralbidv 3121 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) |
41 | 35, 40 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))) |
42 | 41, 28, 34 | rspcdva 3552 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) |
43 | 42 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) |
44 | 34, 43 | mpdan 687 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) |
45 | 44 | simpld 498 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑌:(1...𝐾)⟶(1...𝑁)) |
46 | 45 | ffnd 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 Fn (1...𝐾)) |
47 | 46 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑌 Fn (1...𝐾)) |
48 | | eqfnfv 6871 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 Fn (1...𝐾) ∧ 𝑌 Fn (1...𝐾)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))) |
49 | 33, 47, 48 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))) |
50 | 49 | bicomd 226 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) ↔ 𝑋 = 𝑌)) |
51 | 50 | biimpd 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) → 𝑋 = 𝑌)) |
52 | 51 | syldbl2 841 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 = 𝑌) |
53 | 14, 52 | sylan2b 597 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅) → 𝑋 = 𝑌) |
54 | 53 | ex 416 |
. . . . . . . . . 10
⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ → 𝑋 = 𝑌)) |
55 | 54 | necon3d 2962 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ≠ 𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)) |
56 | 55 | imp 410 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅) |
57 | 10, 56 | mpdan 687 |
. . . . . . 7
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅) |
58 | | fz1ssnn 13168 |
. . . . . . . . . 10
⊢
(1...𝐾) ⊆
ℕ |
59 | 58 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝐾) ⊆ ℕ) |
60 | | nnssre 11859 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ |
61 | 60 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℕ ⊆
ℝ) |
62 | 59, 61 | sstrd 3926 |
. . . . . . . 8
⊢ (𝜑 → (1...𝐾) ⊆ ℝ) |
63 | 7, 62 | sstrd 3926 |
. . . . . . 7
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ) |
64 | 9, 57, 63 | 3jca 1130 |
. . . . . 6
⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) |
65 | | fiinfcl 9142 |
. . . . . 6
⊢ (( <
Or ℝ ∧ ({𝑧 ∈
(1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) |
66 | 4, 64, 65 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) |
67 | 2, 66 | eqeltrd 2839 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) |
68 | 7, 66 | sseldd 3917 |
. . . . . 6
⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾)) |
69 | 2 | eleq1d 2823 |
. . . . . 6
⊢ (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾))) |
70 | 68, 69 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (1...𝐾)) |
71 | | fveq2 6736 |
. . . . . . 7
⊢ (𝑧 = 𝐼 → (𝑋‘𝑧) = (𝑋‘𝐼)) |
72 | | fveq2 6736 |
. . . . . . 7
⊢ (𝑧 = 𝐼 → (𝑌‘𝑧) = (𝑌‘𝐼)) |
73 | 71, 72 | neeq12d 3003 |
. . . . . 6
⊢ (𝑧 = 𝐼 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) |
74 | 73 | elrab3 3616 |
. . . . 5
⊢ (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) |
75 | 70, 74 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) |
76 | 67, 75 | mpbid 235 |
. . 3
⊢ (𝜑 → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) |
77 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑎𝜑 |
78 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑎(1...𝑁) |
79 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑎ℝ |
80 | | elfznn 13166 |
. . . . . . . . 9
⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ) |
81 | 80 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ) |
82 | | nnre 11862 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℝ) |
83 | 81, 82 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ) |
84 | 83 | ex 416 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ)) |
85 | 77, 78, 79, 84 | ssrd 3921 |
. . . . 5
⊢ (𝜑 → (1...𝑁) ⊆ ℝ) |
86 | 31, 70 | ffvelrnd 6924 |
. . . . 5
⊢ (𝜑 → (𝑋‘𝐼) ∈ (1...𝑁)) |
87 | 85, 86 | sseldd 3917 |
. . . 4
⊢ (𝜑 → (𝑋‘𝐼) ∈ ℝ) |
88 | 45, 70 | ffvelrnd 6924 |
. . . . 5
⊢ (𝜑 → (𝑌‘𝐼) ∈ (1...𝑁)) |
89 | 85, 88 | sseldd 3917 |
. . . 4
⊢ (𝜑 → (𝑌‘𝐼) ∈ ℝ) |
90 | | lttri2 10940 |
. . . 4
⊢ (((𝑋‘𝐼) ∈ ℝ ∧ (𝑌‘𝐼) ∈ ℝ) → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))) |
91 | 87, 89, 90 | syl2anc 587 |
. . 3
⊢ (𝜑 → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))) |
92 | 76, 91 | mpbid 235 |
. 2
⊢ (𝜑 → ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) |
93 | 31 | ffund 6568 |
. . . . . 6
⊢ (𝜑 → Fun 𝑋) |
94 | 93 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → Fun 𝑋) |
95 | 31 | fdmd 6575 |
. . . . . . 7
⊢ (𝜑 → dom 𝑋 = (1...𝐾)) |
96 | 70, 95 | eleqtrrd 2842 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ dom 𝑋) |
97 | 96 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → 𝐼 ∈ dom 𝑋) |
98 | | fvelrn 6916 |
. . . . 5
⊢ ((Fun
𝑋 ∧ 𝐼 ∈ dom 𝑋) → (𝑋‘𝐼) ∈ ran 𝑋) |
99 | 94, 97, 98 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∈ ran 𝑋) |
100 | | elfznn 13166 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ) |
101 | 100 | 3ad2ant3 1137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ) |
102 | 101 | nnred 11870 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ) |
103 | 62, 70 | sseldd 3917 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℝ) |
104 | 103 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ) |
105 | 102, 104 | lttri4d 10998 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) |
106 | 45 | 3ad2ant1 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁)) |
107 | | simp3 1140 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾)) |
108 | 106, 107 | ffvelrnd 6924 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ (1...𝑁)) |
109 | | fz1ssnn 13168 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑁) ⊆
ℕ |
110 | 109 | sseli 3911 |
. . . . . . . . . . . . . 14
⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℕ) |
111 | | nnre 11862 |
. . . . . . . . . . . . . 14
⊢ ((𝑌‘𝑗) ∈ ℕ → (𝑌‘𝑗) ∈ ℝ) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℝ) |
113 | 108, 112 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ ℝ) |
114 | 113 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ∈ ℝ) |
115 | 30 | simprd 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) |
116 | 115 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) |
117 | 116 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) |
118 | | simpl3 1195 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾)) |
119 | 70 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾)) |
120 | 119 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾)) |
121 | | breq1 5071 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑗 → (𝑥 < 𝑦 ↔ 𝑗 < 𝑦)) |
122 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑗 → (𝑋‘𝑥) = (𝑋‘𝑗)) |
123 | 122 | breq1d 5078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑗 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝑦))) |
124 | 121, 123 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)))) |
125 | | breq2 5072 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐼 → (𝑗 < 𝑦 ↔ 𝑗 < 𝐼)) |
126 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐼 → (𝑋‘𝑦) = (𝑋‘𝐼)) |
127 | 126 | breq2d 5080 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐼 → ((𝑋‘𝑗) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝐼))) |
128 | 125, 127 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))) |
129 | 124, 128 | rspc2v 3560 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))) |
130 | 118, 120,
129 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))) |
131 | 117, 130 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))) |
132 | 131 | syldbl2 841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑋‘𝐼)) |
133 | | simp2 1139 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾)) |
134 | | simp3 1140 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼) |
135 | 100 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ) |
136 | 135 | nnred 11870 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ) |
137 | 103 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ) |
138 | 136, 137 | ltnled 11004 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼 ≤ 𝑗)) |
139 | 134, 138 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼 ≤ 𝑗) |
140 | 63 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ) |
141 | 9 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) |
142 | | infrefilb 11843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗) |
143 | 142 | 3expia 1123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)) |
144 | 140, 141,
143 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)) |
145 | 144 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗) |
146 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < )) |
147 | 146 | breq1d 5078 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → (𝐼 ≤ 𝑗 ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)) |
148 | 145, 147 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 ≤ 𝑗) |
149 | 148 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → 𝐼 ≤ 𝑗)) |
150 | 149 | con3d 155 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝐼 ≤ 𝑗 → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})) |
151 | 139, 150 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) |
152 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑧𝑗 |
153 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑧(1...𝐾) |
154 | | nfv 1922 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑧(𝑋‘𝑗) ≠ (𝑌‘𝑗) |
155 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑗 → (𝑋‘𝑧) = (𝑋‘𝑗)) |
156 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑗 → (𝑌‘𝑧) = (𝑌‘𝑗)) |
157 | 155, 156 | neeq12d 3003 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑗 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
158 | 152, 153,
154, 157 | elrabf 3611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
159 | 158 | notbii 323 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
160 | | ianor 982 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
161 | 159, 160 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
162 | 151, 161 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
163 | | imor 853 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
164 | 162, 163 | sylibr 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) |
165 | 164 | imp 410 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) |
166 | | nne 2945 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝑋‘𝑗) ≠ (𝑌‘𝑗) ↔ (𝑋‘𝑗) = (𝑌‘𝑗)) |
167 | 165, 166 | sylib 221 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) = (𝑌‘𝑗)) |
168 | 133, 167 | mpdan 687 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) |
169 | 168 | 3expa 1120 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) |
170 | 169 | 3adantl2 1169 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) |
171 | 170 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) = (𝑋‘𝑗)) |
172 | 171 | breq1d 5078 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌‘𝑗) < (𝑋‘𝐼) ↔ (𝑋‘𝑗) < (𝑋‘𝐼))) |
173 | 132, 172 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑋‘𝐼)) |
174 | 114, 173 | ltned 10993 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) |
175 | 76 | 3ad2ant1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) |
176 | 175 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) |
177 | 176 | necomd 2997 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼)) |
178 | | fveq2 6736 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝐼 → (𝑌‘𝑗) = (𝑌‘𝐼)) |
179 | 178 | neeq1d 3001 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝐼 → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼))) |
180 | 179 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼))) |
181 | 177, 180 | mpbird 260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) |
182 | 87 | 3ad2ant1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ) |
183 | 182 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ) |
184 | 89 | 3ad2ant1 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ) |
185 | 184 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ) |
186 | 113 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ∈ ℝ) |
187 | | simpl2 1194 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝐼)) |
188 | 42 | simprd 499 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) |
189 | 188 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) |
190 | 189 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) |
191 | 119 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾)) |
192 | 107 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾)) |
193 | | breq1 5071 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐼 → (𝑥 < 𝑦 ↔ 𝐼 < 𝑦)) |
194 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐼 → (𝑌‘𝑥) = (𝑌‘𝐼)) |
195 | 194 | breq1d 5078 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐼 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑦))) |
196 | 193, 195 | imbi12d 348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)))) |
197 | | breq2 5072 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑗 → (𝐼 < 𝑦 ↔ 𝐼 < 𝑗)) |
198 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑗 → (𝑌‘𝑦) = (𝑌‘𝑗)) |
199 | 198 | breq2d 5080 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑗 → ((𝑌‘𝐼) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑗))) |
200 | 197, 199 | imbi12d 348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))) |
201 | 196, 200 | rspc2v 3560 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))) |
202 | 191, 192,
201 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))) |
203 | 190, 202 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))) |
204 | 203 | syldbl2 841 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑌‘𝑗)) |
205 | 183, 185,
186, 187, 204 | lttrd 11018 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝑗)) |
206 | 183, 205 | ltned 10993 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ≠ (𝑌‘𝑗)) |
207 | 206 | necomd 2997 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) |
208 | 174, 181,
207 | 3jaodan 1432 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) |
209 | 105, 208 | mpdan 687 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) |
210 | 209 | 3expa 1120 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) |
211 | 210 | neneqd 2946 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌‘𝑗) = (𝑋‘𝐼)) |
212 | 211 | ralrimiva 3106 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼)) |
213 | | ralnex 3162 |
. . . . . . . 8
⊢
(∀𝑗 ∈
(1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)) |
214 | 213 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) |
215 | | nnel 3056 |
. . . . . . . . . 10
⊢ (¬
(𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌) |
216 | 215 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌)) |
217 | | fvelrnb 6792 |
. . . . . . . . . 10
⊢ (𝑌 Fn (1...𝐾) → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) |
218 | 46, 217 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) |
219 | 216, 218 | bitrd 282 |
. . . . . . . 8
⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) |
220 | 219 | con1bid 359 |
. . . . . . 7
⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌)) |
221 | 214, 220 | bitrd 282 |
. . . . . 6
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌)) |
222 | 221 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌)) |
223 | 212, 222 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∉ ran 𝑌) |
224 | | elnelne1 3057 |
. . . 4
⊢ (((𝑋‘𝐼) ∈ ran 𝑋 ∧ (𝑋‘𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌) |
225 | 99, 223, 224 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ran 𝑋 ≠ ran 𝑌) |
226 | 45 | ffund 6568 |
. . . . . 6
⊢ (𝜑 → Fun 𝑌) |
227 | 226 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → Fun 𝑌) |
228 | 45 | fdmd 6575 |
. . . . . . 7
⊢ (𝜑 → dom 𝑌 = (1...𝐾)) |
229 | 70, 228 | eleqtrrd 2842 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ dom 𝑌) |
230 | 229 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → 𝐼 ∈ dom 𝑌) |
231 | | fvelrn 6916 |
. . . . 5
⊢ ((Fun
𝑌 ∧ 𝐼 ∈ dom 𝑌) → (𝑌‘𝐼) ∈ ran 𝑌) |
232 | 227, 230,
231 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∈ ran 𝑌) |
233 | 100 | 3ad2ant3 1137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ) |
234 | 233 | nnred 11870 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ) |
235 | 103 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ) |
236 | 234, 235 | lttri4d 10998 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) |
237 | 31 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁)) |
238 | | simp3 1140 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾)) |
239 | 237, 238 | ffvelrnd 6924 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ (1...𝑁)) |
240 | 109 | sseli 3911 |
. . . . . . . . . . . . . 14
⊢ ((𝑋‘𝑗) ∈ (1...𝑁) → (𝑋‘𝑗) ∈ ℕ) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℕ) |
242 | 241 | nnred 11870 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℝ) |
243 | 242 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ∈ ℝ) |
244 | 188 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) |
245 | 244 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) |
246 | | simpl3 1195 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾)) |
247 | 70 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾)) |
248 | 247 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾)) |
249 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑗 → (𝑌‘𝑥) = (𝑌‘𝑗)) |
250 | 249 | breq1d 5078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑗 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝑦))) |
251 | 121, 250 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)))) |
252 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐼 → (𝑌‘𝑦) = (𝑌‘𝐼)) |
253 | 252 | breq2d 5080 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐼 → ((𝑌‘𝑗) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝐼))) |
254 | 125, 253 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))) |
255 | 251, 254 | rspc2v 3560 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))) |
256 | 246, 248,
255 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))) |
257 | 245, 256 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))) |
258 | 257 | syldbl2 841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑌‘𝐼)) |
259 | 169 | 3adantl2 1169 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) |
260 | 259 | breq1d 5078 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋‘𝑗) < (𝑌‘𝐼) ↔ (𝑌‘𝑗) < (𝑌‘𝐼))) |
261 | 258, 260 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑌‘𝐼)) |
262 | 243, 261 | ltned 10993 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) |
263 | 89 | 3ad2ant1 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ) |
264 | 263 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ∈ ℝ) |
265 | | simpl2 1194 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) < (𝑋‘𝐼)) |
266 | 264, 265 | ltned 10993 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼)) |
267 | 266 | necomd 2997 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) |
268 | | fveq2 6736 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝐼 → (𝑋‘𝑗) = (𝑋‘𝐼)) |
269 | 268 | neeq1d 3001 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝐼 → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) |
270 | 269 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) |
271 | 267, 270 | mpbird 260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) |
272 | 263 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ) |
273 | 87 | 3ad2ant1 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ) |
274 | 273 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ) |
275 | 242 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ∈ ℝ) |
276 | | simpl2 1194 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝐼)) |
277 | 115 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) |
278 | 277 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) |
279 | 247 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾)) |
280 | 238 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾)) |
281 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐼 → (𝑋‘𝑥) = (𝑋‘𝐼)) |
282 | 281 | breq1d 5078 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐼 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑦))) |
283 | 193, 282 | imbi12d 348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)))) |
284 | | fveq2 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑗 → (𝑋‘𝑦) = (𝑋‘𝑗)) |
285 | 284 | breq2d 5080 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑗 → ((𝑋‘𝐼) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑗))) |
286 | 197, 285 | imbi12d 348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))) |
287 | 283, 286 | rspc2v 3560 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))) |
288 | 279, 280,
287 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))) |
289 | 278, 288 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))) |
290 | 289 | syldbl2 841 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑋‘𝑗)) |
291 | 272, 274,
275, 276, 290 | lttrd 11018 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝑗)) |
292 | 272, 291 | ltned 10993 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ≠ (𝑋‘𝑗)) |
293 | 292 | necomd 2997 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) |
294 | 262, 271,
293 | 3jaodan 1432 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) |
295 | 236, 294 | mpdan 687 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) |
296 | 295 | 3expa 1120 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) |
297 | 296 | neneqd 2946 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) = (𝑌‘𝐼)) |
298 | 297 | ralrimiva 3106 |
. . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼)) |
299 | | ralnex 3162 |
. . . . . . . 8
⊢
(∀𝑗 ∈
(1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)) |
300 | 299 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) |
301 | | nnel 3056 |
. . . . . . . . . 10
⊢ (¬
(𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋) |
302 | 301 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋)) |
303 | | fvelrnb 6792 |
. . . . . . . . . 10
⊢ (𝑋 Fn (1...𝐾) → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) |
304 | 32, 303 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) |
305 | 302, 304 | bitrd 282 |
. . . . . . . 8
⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) |
306 | 305 | con1bid 359 |
. . . . . . 7
⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋)) |
307 | 300, 306 | bitrd 282 |
. . . . . 6
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋)) |
308 | 307 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋)) |
309 | 298, 308 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∉ ran 𝑋) |
310 | | elnelne1 3057 |
. . . . 5
⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋) |
311 | 310 | necomd 2997 |
. . . 4
⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌) |
312 | 232, 309,
311 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ran 𝑋 ≠ ran 𝑌) |
313 | 225, 312 | jaodan 958 |
. 2
⊢ ((𝜑 ∧ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) → ran 𝑋 ≠ ran 𝑌) |
314 | 92, 313 | mpdan 687 |
1
⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌) |