| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sticksstones1.7 | . . . . . 6
⊢ 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) | 
| 2 | 1 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < )) | 
| 3 |  | ltso 11342 | . . . . . . 7
⊢  < Or
ℝ | 
| 4 | 3 | a1i 11 | . . . . . 6
⊢ (𝜑 → < Or
ℝ) | 
| 5 |  | fzfid 14015 | . . . . . . . 8
⊢ (𝜑 → (1...𝐾) ∈ Fin) | 
| 6 |  | ssrab2 4079 | . . . . . . . . 9
⊢ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾) | 
| 7 | 6 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) | 
| 8 |  | ssfi 9214 | . . . . . . . 8
⊢
(((1...𝐾) ∈ Fin
∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) | 
| 9 | 5, 7, 8 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) | 
| 10 |  | sticksstones1.6 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ≠ 𝑌) | 
| 11 |  | rabeq0 4387 | . . . . . . . . . . . . 13
⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧)) | 
| 12 |  | nne 2943 | . . . . . . . . . . . . . 14
⊢ (¬
(𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑧) = (𝑌‘𝑧)) | 
| 13 | 12 | ralbii 3092 | . . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
(1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) | 
| 14 | 11, 13 | bitri 275 | . . . . . . . . . . . 12
⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) | 
| 15 |  | feq1 6715 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁))) | 
| 16 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑋 → (𝑓‘𝑥) = (𝑋‘𝑥)) | 
| 17 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑋 → (𝑓‘𝑦) = (𝑋‘𝑦)) | 
| 18 | 16, 17 | breq12d 5155 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑋 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑋‘𝑥) < (𝑋‘𝑦))) | 
| 19 | 18 | imbi2d 340 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))) | 
| 20 | 19 | 2ralbidv 3220 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑋 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))) | 
| 21 | 15, 20 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑋 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))) | 
| 22 |  | sticksstones1.3 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} | 
| 23 |  | eqabb 2880 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))) | 
| 24 | 22, 23 | mpbi 230 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) | 
| 25 | 24 | spi 2183 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) | 
| 26 | 25 | biimpi 216 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ 𝐴 → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) | 
| 28 | 27 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑓 ∈ 𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))) | 
| 29 |  | sticksstones1.4 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ 𝐴) | 
| 30 | 21, 28, 29 | rspcdva 3622 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))) | 
| 31 | 30 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋:(1...𝐾)⟶(1...𝑁)) | 
| 32 | 31 | ffnd 6736 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 Fn (1...𝐾)) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 Fn (1...𝐾)) | 
| 34 |  | sticksstones1.5 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑌 ∈ 𝐴) | 
| 35 |  | feq1 6715 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑌 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑌:(1...𝐾)⟶(1...𝑁))) | 
| 36 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑌 → (𝑓‘𝑥) = (𝑌‘𝑥)) | 
| 37 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑌 → (𝑓‘𝑦) = (𝑌‘𝑦)) | 
| 38 | 36, 37 | breq12d 5155 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑌 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑌‘𝑥) < (𝑌‘𝑦))) | 
| 39 | 38 | imbi2d 340 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) | 
| 40 | 39 | 2ralbidv 3220 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) | 
| 41 | 35, 40 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))) | 
| 42 | 41, 28, 34 | rspcdva 3622 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) | 
| 44 | 34, 43 | mpdan 687 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))) | 
| 45 | 44 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑌:(1...𝐾)⟶(1...𝑁)) | 
| 46 | 45 | ffnd 6736 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 Fn (1...𝐾)) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑌 Fn (1...𝐾)) | 
| 48 |  | eqfnfv 7050 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 Fn (1...𝐾) ∧ 𝑌 Fn (1...𝐾)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))) | 
| 49 | 33, 47, 48 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))) | 
| 50 | 49 | bicomd 223 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) ↔ 𝑋 = 𝑌)) | 
| 51 | 50 | biimpd 229 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) → 𝑋 = 𝑌)) | 
| 52 | 51 | syldbl2 841 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 = 𝑌) | 
| 53 | 14, 52 | sylan2b 594 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅) → 𝑋 = 𝑌) | 
| 54 | 53 | ex 412 | . . . . . . . . . 10
⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ → 𝑋 = 𝑌)) | 
| 55 | 54 | necon3d 2960 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 ≠ 𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)) | 
| 56 | 55 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅) | 
| 57 | 10, 56 | mpdan 687 | . . . . . . 7
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅) | 
| 58 |  | fz1ssnn 13596 | . . . . . . . . . 10
⊢
(1...𝐾) ⊆
ℕ | 
| 59 | 58 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (1...𝐾) ⊆ ℕ) | 
| 60 |  | nnssre 12271 | . . . . . . . . . 10
⊢ ℕ
⊆ ℝ | 
| 61 | 60 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℕ ⊆
ℝ) | 
| 62 | 59, 61 | sstrd 3993 | . . . . . . . 8
⊢ (𝜑 → (1...𝐾) ⊆ ℝ) | 
| 63 | 7, 62 | sstrd 3993 | . . . . . . 7
⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ) | 
| 64 | 9, 57, 63 | 3jca 1128 | . . . . . 6
⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) | 
| 65 |  | fiinfcl 9542 | . . . . . 6
⊢ (( <
Or ℝ ∧ ({𝑧 ∈
(1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) | 
| 66 | 4, 64, 65 | syl2anc 584 | . . . . 5
⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) | 
| 67 | 2, 66 | eqeltrd 2840 | . . . 4
⊢ (𝜑 → 𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) | 
| 68 | 7, 66 | sseldd 3983 | . . . . . 6
⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾)) | 
| 69 | 2 | eleq1d 2825 | . . . . . 6
⊢ (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾))) | 
| 70 | 68, 69 | mpbird 257 | . . . . 5
⊢ (𝜑 → 𝐼 ∈ (1...𝐾)) | 
| 71 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑧 = 𝐼 → (𝑋‘𝑧) = (𝑋‘𝐼)) | 
| 72 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑧 = 𝐼 → (𝑌‘𝑧) = (𝑌‘𝐼)) | 
| 73 | 71, 72 | neeq12d 3001 | . . . . . 6
⊢ (𝑧 = 𝐼 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) | 
| 74 | 73 | elrab3 3692 | . . . . 5
⊢ (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) | 
| 75 | 70, 74 | syl 17 | . . . 4
⊢ (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) | 
| 76 | 67, 75 | mpbid 232 | . . 3
⊢ (𝜑 → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) | 
| 77 |  | nfv 1913 | . . . . . 6
⊢
Ⅎ𝑎𝜑 | 
| 78 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑎(1...𝑁) | 
| 79 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑎ℝ | 
| 80 |  | elfznn 13594 | . . . . . . . . 9
⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ) | 
| 81 | 80 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ) | 
| 82 |  | nnre 12274 | . . . . . . . 8
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℝ) | 
| 83 | 81, 82 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ) | 
| 84 | 83 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ)) | 
| 85 | 77, 78, 79, 84 | ssrd 3987 | . . . . 5
⊢ (𝜑 → (1...𝑁) ⊆ ℝ) | 
| 86 | 31, 70 | ffvelcdmd 7104 | . . . . 5
⊢ (𝜑 → (𝑋‘𝐼) ∈ (1...𝑁)) | 
| 87 | 85, 86 | sseldd 3983 | . . . 4
⊢ (𝜑 → (𝑋‘𝐼) ∈ ℝ) | 
| 88 | 45, 70 | ffvelcdmd 7104 | . . . . 5
⊢ (𝜑 → (𝑌‘𝐼) ∈ (1...𝑁)) | 
| 89 | 85, 88 | sseldd 3983 | . . . 4
⊢ (𝜑 → (𝑌‘𝐼) ∈ ℝ) | 
| 90 |  | lttri2 11344 | . . . 4
⊢ (((𝑋‘𝐼) ∈ ℝ ∧ (𝑌‘𝐼) ∈ ℝ) → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))) | 
| 91 | 87, 89, 90 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))) | 
| 92 | 76, 91 | mpbid 232 | . 2
⊢ (𝜑 → ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) | 
| 93 | 31 | ffund 6739 | . . . . . 6
⊢ (𝜑 → Fun 𝑋) | 
| 94 | 93 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → Fun 𝑋) | 
| 95 | 31 | fdmd 6745 | . . . . . . 7
⊢ (𝜑 → dom 𝑋 = (1...𝐾)) | 
| 96 | 70, 95 | eleqtrrd 2843 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ dom 𝑋) | 
| 97 | 96 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → 𝐼 ∈ dom 𝑋) | 
| 98 |  | fvelrn 7095 | . . . . 5
⊢ ((Fun
𝑋 ∧ 𝐼 ∈ dom 𝑋) → (𝑋‘𝐼) ∈ ran 𝑋) | 
| 99 | 94, 97, 98 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∈ ran 𝑋) | 
| 100 |  | elfznn 13594 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ) | 
| 101 | 100 | 3ad2ant3 1135 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ) | 
| 102 | 101 | nnred 12282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ) | 
| 103 | 62, 70 | sseldd 3983 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℝ) | 
| 104 | 103 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ) | 
| 105 | 102, 104 | lttri4d 11403 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) | 
| 106 | 45 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁)) | 
| 107 |  | simp3 1138 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾)) | 
| 108 | 106, 107 | ffvelcdmd 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ (1...𝑁)) | 
| 109 |  | fz1ssnn 13596 | . . . . . . . . . . . . . . 15
⊢
(1...𝑁) ⊆
ℕ | 
| 110 | 109 | sseli 3978 | . . . . . . . . . . . . . 14
⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℕ) | 
| 111 |  | nnre 12274 | . . . . . . . . . . . . . 14
⊢ ((𝑌‘𝑗) ∈ ℕ → (𝑌‘𝑗) ∈ ℝ) | 
| 112 | 110, 111 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℝ) | 
| 113 | 108, 112 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ ℝ) | 
| 114 | 113 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ∈ ℝ) | 
| 115 | 30 | simprd 495 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) | 
| 116 | 115 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) | 
| 117 | 116 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) | 
| 118 |  | simpl3 1193 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾)) | 
| 119 | 70 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾)) | 
| 120 | 119 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾)) | 
| 121 |  | breq1 5145 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑗 → (𝑥 < 𝑦 ↔ 𝑗 < 𝑦)) | 
| 122 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑗 → (𝑋‘𝑥) = (𝑋‘𝑗)) | 
| 123 | 122 | breq1d 5152 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑗 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝑦))) | 
| 124 | 121, 123 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)))) | 
| 125 |  | breq2 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐼 → (𝑗 < 𝑦 ↔ 𝑗 < 𝐼)) | 
| 126 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐼 → (𝑋‘𝑦) = (𝑋‘𝐼)) | 
| 127 | 126 | breq2d 5154 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐼 → ((𝑋‘𝑗) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝐼))) | 
| 128 | 125, 127 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))) | 
| 129 | 124, 128 | rspc2v 3632 | . . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))) | 
| 130 | 118, 120,
129 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))) | 
| 131 | 117, 130 | mpd 15 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))) | 
| 132 | 131 | syldbl2 841 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑋‘𝐼)) | 
| 133 |  | simp2 1137 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾)) | 
| 134 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼) | 
| 135 | 100 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ) | 
| 136 | 135 | nnred 12282 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ) | 
| 137 | 103 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ) | 
| 138 | 136, 137 | ltnled 11409 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼 ≤ 𝑗)) | 
| 139 | 134, 138 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼 ≤ 𝑗) | 
| 140 | 63 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ) | 
| 141 | 9 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) | 
| 142 |  | infrefilb 12255 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗) | 
| 143 | 142 | 3expia 1121 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)) | 
| 144 | 140, 141,
143 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)) | 
| 145 | 144 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗) | 
| 146 | 1 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < )) | 
| 147 | 146 | breq1d 5152 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → (𝐼 ≤ 𝑗 ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)) | 
| 148 | 145, 147 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 ≤ 𝑗) | 
| 149 | 148 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → 𝐼 ≤ 𝑗)) | 
| 150 | 149 | con3d 152 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝐼 ≤ 𝑗 → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})) | 
| 151 | 139, 150 | mpd 15 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) | 
| 152 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑧𝑗 | 
| 153 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑧(1...𝐾) | 
| 154 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑧(𝑋‘𝑗) ≠ (𝑌‘𝑗) | 
| 155 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑗 → (𝑋‘𝑧) = (𝑋‘𝑗)) | 
| 156 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑗 → (𝑌‘𝑧) = (𝑌‘𝑗)) | 
| 157 | 155, 156 | neeq12d 3001 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑗 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 158 | 152, 153,
154, 157 | elrabf 3687 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 159 | 158 | notbii 320 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 160 |  | ianor 983 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
(𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 161 | 159, 160 | bitri 275 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 162 | 151, 161 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 163 |  | imor 853 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 164 | 162, 163 | sylibr 234 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))) | 
| 165 | 164 | imp 406 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) | 
| 166 |  | nne 2943 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝑋‘𝑗) ≠ (𝑌‘𝑗) ↔ (𝑋‘𝑗) = (𝑌‘𝑗)) | 
| 167 | 165, 166 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) = (𝑌‘𝑗)) | 
| 168 | 133, 167 | mpdan 687 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) | 
| 169 | 168 | 3expa 1118 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) | 
| 170 | 169 | 3adantl2 1167 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) | 
| 171 | 170 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) = (𝑋‘𝑗)) | 
| 172 | 171 | breq1d 5152 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌‘𝑗) < (𝑋‘𝐼) ↔ (𝑋‘𝑗) < (𝑋‘𝐼))) | 
| 173 | 132, 172 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑋‘𝐼)) | 
| 174 | 114, 173 | ltned 11398 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) | 
| 175 | 76 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) | 
| 176 | 175 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) | 
| 177 | 176 | necomd 2995 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼)) | 
| 178 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝐼 → (𝑌‘𝑗) = (𝑌‘𝐼)) | 
| 179 | 178 | neeq1d 2999 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝐼 → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼))) | 
| 180 | 179 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼))) | 
| 181 | 177, 180 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) | 
| 182 | 87 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ) | 
| 183 | 182 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ) | 
| 184 | 89 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ) | 
| 185 | 184 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ) | 
| 186 | 113 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ∈ ℝ) | 
| 187 |  | simpl2 1192 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝐼)) | 
| 188 | 42 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) | 
| 189 | 188 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) | 
| 190 | 189 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) | 
| 191 | 119 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾)) | 
| 192 | 107 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾)) | 
| 193 |  | breq1 5145 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐼 → (𝑥 < 𝑦 ↔ 𝐼 < 𝑦)) | 
| 194 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐼 → (𝑌‘𝑥) = (𝑌‘𝐼)) | 
| 195 | 194 | breq1d 5152 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐼 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑦))) | 
| 196 | 193, 195 | imbi12d 344 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)))) | 
| 197 |  | breq2 5146 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑗 → (𝐼 < 𝑦 ↔ 𝐼 < 𝑗)) | 
| 198 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑗 → (𝑌‘𝑦) = (𝑌‘𝑗)) | 
| 199 | 198 | breq2d 5154 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑗 → ((𝑌‘𝐼) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑗))) | 
| 200 | 197, 199 | imbi12d 344 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))) | 
| 201 | 196, 200 | rspc2v 3632 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))) | 
| 202 | 191, 192,
201 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))) | 
| 203 | 190, 202 | mpd 15 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))) | 
| 204 | 203 | syldbl2 841 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑌‘𝑗)) | 
| 205 | 183, 185,
186, 187, 204 | lttrd 11423 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝑗)) | 
| 206 | 183, 205 | ltned 11398 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ≠ (𝑌‘𝑗)) | 
| 207 | 206 | necomd 2995 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) | 
| 208 | 174, 181,
207 | 3jaodan 1432 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) | 
| 209 | 105, 208 | mpdan 687 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) | 
| 210 | 209 | 3expa 1118 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼)) | 
| 211 | 210 | neneqd 2944 | . . . . . 6
⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌‘𝑗) = (𝑋‘𝐼)) | 
| 212 | 211 | ralrimiva 3145 | . . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼)) | 
| 213 |  | ralnex 3071 | . . . . . . . 8
⊢
(∀𝑗 ∈
(1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)) | 
| 214 | 213 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) | 
| 215 |  | nnel 3055 | . . . . . . . . . 10
⊢ (¬
(𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌) | 
| 216 | 215 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌)) | 
| 217 |  | fvelrnb 6968 | . . . . . . . . . 10
⊢ (𝑌 Fn (1...𝐾) → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) | 
| 218 | 46, 217 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) | 
| 219 | 216, 218 | bitrd 279 | . . . . . . . 8
⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))) | 
| 220 | 219 | con1bid 355 | . . . . . . 7
⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌)) | 
| 221 | 214, 220 | bitrd 279 | . . . . . 6
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌)) | 
| 222 | 221 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌)) | 
| 223 | 212, 222 | mpbid 232 | . . . 4
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∉ ran 𝑌) | 
| 224 |  | elnelne1 3056 | . . . 4
⊢ (((𝑋‘𝐼) ∈ ran 𝑋 ∧ (𝑋‘𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌) | 
| 225 | 99, 223, 224 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ran 𝑋 ≠ ran 𝑌) | 
| 226 | 45 | ffund 6739 | . . . . . 6
⊢ (𝜑 → Fun 𝑌) | 
| 227 | 226 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → Fun 𝑌) | 
| 228 | 45 | fdmd 6745 | . . . . . . 7
⊢ (𝜑 → dom 𝑌 = (1...𝐾)) | 
| 229 | 70, 228 | eleqtrrd 2843 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ dom 𝑌) | 
| 230 | 229 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → 𝐼 ∈ dom 𝑌) | 
| 231 |  | fvelrn 7095 | . . . . 5
⊢ ((Fun
𝑌 ∧ 𝐼 ∈ dom 𝑌) → (𝑌‘𝐼) ∈ ran 𝑌) | 
| 232 | 227, 230,
231 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∈ ran 𝑌) | 
| 233 | 100 | 3ad2ant3 1135 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ) | 
| 234 | 233 | nnred 12282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ) | 
| 235 | 103 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ) | 
| 236 | 234, 235 | lttri4d 11403 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) | 
| 237 | 31 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁)) | 
| 238 |  | simp3 1138 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾)) | 
| 239 | 237, 238 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ (1...𝑁)) | 
| 240 | 109 | sseli 3978 | . . . . . . . . . . . . . 14
⊢ ((𝑋‘𝑗) ∈ (1...𝑁) → (𝑋‘𝑗) ∈ ℕ) | 
| 241 | 239, 240 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℕ) | 
| 242 | 241 | nnred 12282 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℝ) | 
| 243 | 242 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ∈ ℝ) | 
| 244 | 188 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) | 
| 245 | 244 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))) | 
| 246 |  | simpl3 1193 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾)) | 
| 247 | 70 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾)) | 
| 248 | 247 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾)) | 
| 249 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑗 → (𝑌‘𝑥) = (𝑌‘𝑗)) | 
| 250 | 249 | breq1d 5152 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑗 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝑦))) | 
| 251 | 121, 250 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)))) | 
| 252 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐼 → (𝑌‘𝑦) = (𝑌‘𝐼)) | 
| 253 | 252 | breq2d 5154 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐼 → ((𝑌‘𝑗) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝐼))) | 
| 254 | 125, 253 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))) | 
| 255 | 251, 254 | rspc2v 3632 | . . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))) | 
| 256 | 246, 248,
255 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))) | 
| 257 | 245, 256 | mpd 15 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))) | 
| 258 | 257 | syldbl2 841 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑌‘𝐼)) | 
| 259 | 169 | 3adantl2 1167 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗)) | 
| 260 | 259 | breq1d 5152 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋‘𝑗) < (𝑌‘𝐼) ↔ (𝑌‘𝑗) < (𝑌‘𝐼))) | 
| 261 | 258, 260 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑌‘𝐼)) | 
| 262 | 243, 261 | ltned 11398 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) | 
| 263 | 89 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ) | 
| 264 | 263 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ∈ ℝ) | 
| 265 |  | simpl2 1192 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) < (𝑋‘𝐼)) | 
| 266 | 264, 265 | ltned 11398 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼)) | 
| 267 | 266 | necomd 2995 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼)) | 
| 268 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝐼 → (𝑋‘𝑗) = (𝑋‘𝐼)) | 
| 269 | 268 | neeq1d 2999 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝐼 → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) | 
| 270 | 269 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼))) | 
| 271 | 267, 270 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) | 
| 272 | 263 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ) | 
| 273 | 87 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ) | 
| 274 | 273 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ) | 
| 275 | 242 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ∈ ℝ) | 
| 276 |  | simpl2 1192 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝐼)) | 
| 277 | 115 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) | 
| 278 | 277 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))) | 
| 279 | 247 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾)) | 
| 280 | 238 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾)) | 
| 281 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐼 → (𝑋‘𝑥) = (𝑋‘𝐼)) | 
| 282 | 281 | breq1d 5152 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐼 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑦))) | 
| 283 | 193, 282 | imbi12d 344 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)))) | 
| 284 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑗 → (𝑋‘𝑦) = (𝑋‘𝑗)) | 
| 285 | 284 | breq2d 5154 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑗 → ((𝑋‘𝐼) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑗))) | 
| 286 | 197, 285 | imbi12d 344 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))) | 
| 287 | 283, 286 | rspc2v 3632 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))) | 
| 288 | 279, 280,
287 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))) | 
| 289 | 278, 288 | mpd 15 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))) | 
| 290 | 289 | syldbl2 841 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑋‘𝑗)) | 
| 291 | 272, 274,
275, 276, 290 | lttrd 11423 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝑗)) | 
| 292 | 272, 291 | ltned 11398 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ≠ (𝑋‘𝑗)) | 
| 293 | 292 | necomd 2995 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) | 
| 294 | 262, 271,
293 | 3jaodan 1432 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) | 
| 295 | 236, 294 | mpdan 687 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) | 
| 296 | 295 | 3expa 1118 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼)) | 
| 297 | 296 | neneqd 2944 | . . . . . 6
⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) = (𝑌‘𝐼)) | 
| 298 | 297 | ralrimiva 3145 | . . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼)) | 
| 299 |  | ralnex 3071 | . . . . . . . 8
⊢
(∀𝑗 ∈
(1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)) | 
| 300 | 299 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) | 
| 301 |  | nnel 3055 | . . . . . . . . . 10
⊢ (¬
(𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋) | 
| 302 | 301 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋)) | 
| 303 |  | fvelrnb 6968 | . . . . . . . . . 10
⊢ (𝑋 Fn (1...𝐾) → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) | 
| 304 | 32, 303 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) | 
| 305 | 302, 304 | bitrd 279 | . . . . . . . 8
⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))) | 
| 306 | 305 | con1bid 355 | . . . . . . 7
⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋)) | 
| 307 | 300, 306 | bitrd 279 | . . . . . 6
⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋)) | 
| 308 | 307 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋)) | 
| 309 | 298, 308 | mpbid 232 | . . . 4
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∉ ran 𝑋) | 
| 310 |  | elnelne1 3056 | . . . . 5
⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋) | 
| 311 | 310 | necomd 2995 | . . . 4
⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌) | 
| 312 | 232, 309,
311 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ran 𝑋 ≠ ran 𝑌) | 
| 313 | 225, 312 | jaodan 959 | . 2
⊢ ((𝜑 ∧ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) → ran 𝑋 ≠ ran 𝑌) | 
| 314 | 92, 313 | mpdan 687 | 1
⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌) |