Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sticksstones1 Structured version   Visualization version   GIF version

Theorem sticksstones1 42128
Description: Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024.)
Hypotheses
Ref Expression
sticksstones1.1 (𝜑𝑁 ∈ ℕ0)
sticksstones1.2 (𝜑𝐾 ∈ ℕ0)
sticksstones1.3 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))}
sticksstones1.4 (𝜑𝑋𝐴)
sticksstones1.5 (𝜑𝑌𝐴)
sticksstones1.6 (𝜑𝑋𝑌)
sticksstones1.7 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < )
Assertion
Ref Expression
sticksstones1 (𝜑 → ran 𝑋 ≠ ran 𝑌)
Distinct variable groups:   𝐴,𝑓   𝑥,𝐼,𝑦   𝑧,𝐼   𝑓,𝐾,𝑥,𝑦   𝑧,𝐾   𝑓,𝑁   𝑓,𝑋,𝑥,𝑦   𝑧,𝑋   𝑓,𝑌,𝑥,𝑦   𝑧,𝑌   𝜑,𝑓
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝐴(𝑥,𝑦,𝑧)   𝐼(𝑓)   𝑁(𝑥,𝑦,𝑧)

Proof of Theorem sticksstones1
Dummy variables 𝑗 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sticksstones1.7 . . . . . 6 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < )
21a1i 11 . . . . 5 (𝜑𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ))
3 ltso 11339 . . . . . . 7 < Or ℝ
43a1i 11 . . . . . 6 (𝜑 → < Or ℝ)
5 fzfid 14011 . . . . . . . 8 (𝜑 → (1...𝐾) ∈ Fin)
6 ssrab2 4090 . . . . . . . . 9 {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ (1...𝐾)
76a1i 11 . . . . . . . 8 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ (1...𝐾))
8 ssfi 9212 . . . . . . . 8 (((1...𝐾) ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin)
95, 7, 8syl2anc 584 . . . . . . 7 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin)
10 sticksstones1.6 . . . . . . . 8 (𝜑𝑋𝑌)
11 rabeq0 4394 . . . . . . . . . . . . 13 ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋𝑧) ≠ (𝑌𝑧))
12 nne 2942 . . . . . . . . . . . . . 14 (¬ (𝑋𝑧) ≠ (𝑌𝑧) ↔ (𝑋𝑧) = (𝑌𝑧))
1312ralbii 3091 . . . . . . . . . . . . 13 (∀𝑧 ∈ (1...𝐾) ¬ (𝑋𝑧) ≠ (𝑌𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧))
1411, 13bitri 275 . . . . . . . . . . . 12 ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧))
15 feq1 6717 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁)))
16 fveq1 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑋 → (𝑓𝑥) = (𝑋𝑥))
17 fveq1 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑋 → (𝑓𝑦) = (𝑋𝑦))
1816, 17breq12d 5161 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑋 → ((𝑓𝑥) < (𝑓𝑦) ↔ (𝑋𝑥) < (𝑋𝑦)))
1918imbi2d 340 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ (𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦))))
20192ralbidv 3219 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝑋 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦))))
2115, 20anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑋 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))) ↔ (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))))
22 sticksstones1.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))}
23 eqabb 2879 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))} ↔ ∀𝑓(𝑓𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))))
2422, 23mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓(𝑓𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2524spi 2182 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2625biimpi 216 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝐴 → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2726adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓𝐴) → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2827ralrimiva 3144 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑓𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
29 sticksstones1.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑋𝐴)
3021, 28, 29rspcdva 3623 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦))))
3130simpld 494 . . . . . . . . . . . . . . . . . 18 (𝜑𝑋:(1...𝐾)⟶(1...𝑁))
3231ffnd 6738 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 Fn (1...𝐾))
3332adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → 𝑋 Fn (1...𝐾))
34 sticksstones1.5 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑌𝐴)
35 feq1 6717 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑌 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑌:(1...𝐾)⟶(1...𝑁)))
36 fveq1 6906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑌 → (𝑓𝑥) = (𝑌𝑥))
37 fveq1 6906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑌 → (𝑓𝑦) = (𝑌𝑦))
3836, 37breq12d 5161 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑌 → ((𝑓𝑥) < (𝑓𝑦) ↔ (𝑌𝑥) < (𝑌𝑦)))
3938imbi2d 340 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ (𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
40392ralbidv 3219 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4135, 40anbi12d 632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))))
4241, 28, 34rspcdva 3623 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4342adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑌𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4434, 43mpdan 687 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4544simpld 494 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌:(1...𝐾)⟶(1...𝑁))
4645ffnd 6738 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 Fn (1...𝐾))
4746adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → 𝑌 Fn (1...𝐾))
48 eqfnfv 7051 . . . . . . . . . . . . . . . 16 ((𝑋 Fn (1...𝐾) ∧ 𝑌 Fn (1...𝐾)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)))
4933, 47, 48syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)))
5049bicomd 223 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧) ↔ 𝑋 = 𝑌))
5150biimpd 229 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧) → 𝑋 = 𝑌))
5251syldbl2 841 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → 𝑋 = 𝑌)
5314, 52sylan2b 594 . . . . . . . . . . 11 ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅) → 𝑋 = 𝑌)
5453ex 412 . . . . . . . . . 10 (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅ → 𝑋 = 𝑌))
5554necon3d 2959 . . . . . . . . 9 (𝜑 → (𝑋𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅))
5655imp 406 . . . . . . . 8 ((𝜑𝑋𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅)
5710, 56mpdan 687 . . . . . . 7 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅)
58 fz1ssnn 13592 . . . . . . . . . 10 (1...𝐾) ⊆ ℕ
5958a1i 11 . . . . . . . . 9 (𝜑 → (1...𝐾) ⊆ ℕ)
60 nnssre 12268 . . . . . . . . . 10 ℕ ⊆ ℝ
6160a1i 11 . . . . . . . . 9 (𝜑 → ℕ ⊆ ℝ)
6259, 61sstrd 4006 . . . . . . . 8 (𝜑 → (1...𝐾) ⊆ ℝ)
637, 62sstrd 4006 . . . . . . 7 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ)
649, 57, 633jca 1127 . . . . . 6 (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ))
65 fiinfcl 9539 . . . . . 6 (( < Or ℝ ∧ ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)})
664, 64, 65syl2anc 584 . . . . 5 (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)})
672, 66eqeltrd 2839 . . . 4 (𝜑𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)})
687, 66sseldd 3996 . . . . . 6 (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ (1...𝐾))
692eleq1d 2824 . . . . . 6 (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ (1...𝐾)))
7068, 69mpbird 257 . . . . 5 (𝜑𝐼 ∈ (1...𝐾))
71 fveq2 6907 . . . . . . 7 (𝑧 = 𝐼 → (𝑋𝑧) = (𝑋𝐼))
72 fveq2 6907 . . . . . . 7 (𝑧 = 𝐼 → (𝑌𝑧) = (𝑌𝐼))
7371, 72neeq12d 3000 . . . . . 6 (𝑧 = 𝐼 → ((𝑋𝑧) ≠ (𝑌𝑧) ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
7473elrab3 3696 . . . . 5 (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
7570, 74syl 17 . . . 4 (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
7667, 75mpbid 232 . . 3 (𝜑 → (𝑋𝐼) ≠ (𝑌𝐼))
77 nfv 1912 . . . . . 6 𝑎𝜑
78 nfcv 2903 . . . . . 6 𝑎(1...𝑁)
79 nfcv 2903 . . . . . 6 𝑎
80 elfznn 13590 . . . . . . . . 9 (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
8180adantl 481 . . . . . . . 8 ((𝜑𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ)
82 nnre 12271 . . . . . . . 8 (𝑎 ∈ ℕ → 𝑎 ∈ ℝ)
8381, 82syl 17 . . . . . . 7 ((𝜑𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ)
8483ex 412 . . . . . 6 (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ))
8577, 78, 79, 84ssrd 4000 . . . . 5 (𝜑 → (1...𝑁) ⊆ ℝ)
8631, 70ffvelcdmd 7105 . . . . 5 (𝜑 → (𝑋𝐼) ∈ (1...𝑁))
8785, 86sseldd 3996 . . . 4 (𝜑 → (𝑋𝐼) ∈ ℝ)
8845, 70ffvelcdmd 7105 . . . . 5 (𝜑 → (𝑌𝐼) ∈ (1...𝑁))
8985, 88sseldd 3996 . . . 4 (𝜑 → (𝑌𝐼) ∈ ℝ)
90 lttri2 11341 . . . 4 (((𝑋𝐼) ∈ ℝ ∧ (𝑌𝐼) ∈ ℝ) → ((𝑋𝐼) ≠ (𝑌𝐼) ↔ ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼))))
9187, 89, 90syl2anc 584 . . 3 (𝜑 → ((𝑋𝐼) ≠ (𝑌𝐼) ↔ ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼))))
9276, 91mpbid 232 . 2 (𝜑 → ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼)))
9331ffund 6741 . . . . . 6 (𝜑 → Fun 𝑋)
9493adantr 480 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → Fun 𝑋)
9531fdmd 6747 . . . . . . 7 (𝜑 → dom 𝑋 = (1...𝐾))
9670, 95eleqtrrd 2842 . . . . . 6 (𝜑𝐼 ∈ dom 𝑋)
9796adantr 480 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → 𝐼 ∈ dom 𝑋)
98 fvelrn 7096 . . . . 5 ((Fun 𝑋𝐼 ∈ dom 𝑋) → (𝑋𝐼) ∈ ran 𝑋)
9994, 97, 98syl2anc 584 . . . 4 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → (𝑋𝐼) ∈ ran 𝑋)
100 elfznn 13590 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ)
1011003ad2ant3 1134 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
102101nnred 12279 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
10362, 70sseldd 3996 . . . . . . . . . . 11 (𝜑𝐼 ∈ ℝ)
1041033ad2ant1 1132 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
105102, 104lttri4d 11400 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗))
106453ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁))
107 simp3 1137 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
108106, 107ffvelcdmd 7105 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ∈ (1...𝑁))
109 fz1ssnn 13592 . . . . . . . . . . . . . . 15 (1...𝑁) ⊆ ℕ
110109sseli 3991 . . . . . . . . . . . . . 14 ((𝑌𝑗) ∈ (1...𝑁) → (𝑌𝑗) ∈ ℕ)
111 nnre 12271 . . . . . . . . . . . . . 14 ((𝑌𝑗) ∈ ℕ → (𝑌𝑗) ∈ ℝ)
112110, 111syl 17 . . . . . . . . . . . . 13 ((𝑌𝑗) ∈ (1...𝑁) → (𝑌𝑗) ∈ ℝ)
113108, 112syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ∈ ℝ)
114113adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) ∈ ℝ)
11530simprd 495 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
1161153ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
117116adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
118 simpl3 1192 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
119703ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
120119adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
121 breq1 5151 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑗 → (𝑥 < 𝑦𝑗 < 𝑦))
122 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑗 → (𝑋𝑥) = (𝑋𝑗))
123122breq1d 5158 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑗 → ((𝑋𝑥) < (𝑋𝑦) ↔ (𝑋𝑗) < (𝑋𝑦)))
124121, 123imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) ↔ (𝑗 < 𝑦 → (𝑋𝑗) < (𝑋𝑦))))
125 breq2 5152 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐼 → (𝑗 < 𝑦𝑗 < 𝐼))
126 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝐼 → (𝑋𝑦) = (𝑋𝐼))
127126breq2d 5160 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐼 → ((𝑋𝑗) < (𝑋𝑦) ↔ (𝑋𝑗) < (𝑋𝐼)))
128125, 127imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋𝑗) < (𝑋𝑦)) ↔ (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼))))
129124, 128rspc2v 3633 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼))))
130118, 120, 129syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼))))
131117, 130mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼)))
132131syldbl2 841 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) < (𝑋𝐼))
133 simp2 1136 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
134 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼)
1351003ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ)
136135nnred 12279 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ)
1371033ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ)
138136, 137ltnled 11406 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼𝑗))
139134, 138mpbid 232 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼𝑗)
140633ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ)
14193ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin)
142 infrefilb 12252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗)
1431423expia 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗))
144140, 141, 143syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗))
145144imp 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗)
1461a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ))
147146breq1d 5158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → (𝐼𝑗 ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗))
148145, 147mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → 𝐼𝑗)
149148ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} → 𝐼𝑗))
150149con3d 152 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝐼𝑗 → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}))
151139, 150mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)})
152 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧𝑗
153 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧(1...𝐾)
154 nfv 1912 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑧(𝑋𝑗) ≠ (𝑌𝑗)
155 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑗 → (𝑋𝑧) = (𝑋𝑗))
156 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑗 → (𝑌𝑧) = (𝑌𝑗))
157155, 156neeq12d 3000 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑗 → ((𝑋𝑧) ≠ (𝑌𝑧) ↔ (𝑋𝑗) ≠ (𝑌𝑗)))
158152, 153, 154, 157elrabf 3691 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋𝑗) ≠ (𝑌𝑗)))
159158notbii 320 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋𝑗) ≠ (𝑌𝑗)))
160 ianor 983 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋𝑗) ≠ (𝑌𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
161159, 160bitri 275 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
162151, 161sylib 218 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
163 imor 853 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ (1...𝐾) → ¬ (𝑋𝑗) ≠ (𝑌𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
164162, 163sylibr 234 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
165164imp 406 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋𝑗) ≠ (𝑌𝑗))
166 nne 2942 . . . . . . . . . . . . . . . . . 18 (¬ (𝑋𝑗) ≠ (𝑌𝑗) ↔ (𝑋𝑗) = (𝑌𝑗))
167165, 166sylib 218 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) = (𝑌𝑗))
168133, 167mpdan 687 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
1691683expa 1117 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
1701693adantl2 1166 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
171170eqcomd 2741 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) = (𝑋𝑗))
172171breq1d 5158 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌𝑗) < (𝑋𝐼) ↔ (𝑋𝑗) < (𝑋𝐼)))
173132, 172mpbird 257 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) < (𝑋𝐼))
174114, 173ltned 11395 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) ≠ (𝑋𝐼))
175763ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝐼) ≠ (𝑌𝐼))
176175adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋𝐼) ≠ (𝑌𝐼))
177176necomd 2994 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) ≠ (𝑋𝐼))
178 fveq2 6907 . . . . . . . . . . . . 13 (𝑗 = 𝐼 → (𝑌𝑗) = (𝑌𝐼))
179178neeq1d 2998 . . . . . . . . . . . 12 (𝑗 = 𝐼 → ((𝑌𝑗) ≠ (𝑋𝐼) ↔ (𝑌𝐼) ≠ (𝑋𝐼)))
180179adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌𝑗) ≠ (𝑋𝐼) ↔ (𝑌𝐼) ≠ (𝑋𝐼)))
181177, 180mpbird 257 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝑗) ≠ (𝑋𝐼))
182873ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝐼) ∈ ℝ)
183182adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) ∈ ℝ)
184893ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝐼) ∈ ℝ)
185184adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) ∈ ℝ)
186113adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝑗) ∈ ℝ)
187 simpl2 1191 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) < (𝑌𝐼))
18842simprd 495 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
1891883ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
190189adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
191119adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
192107adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
193 breq1 5151 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐼 → (𝑥 < 𝑦𝐼 < 𝑦))
194 fveq2 6907 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝐼 → (𝑌𝑥) = (𝑌𝐼))
195194breq1d 5158 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐼 → ((𝑌𝑥) < (𝑌𝑦) ↔ (𝑌𝐼) < (𝑌𝑦)))
196193, 195imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) ↔ (𝐼 < 𝑦 → (𝑌𝐼) < (𝑌𝑦))))
197 breq2 5152 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑗 → (𝐼 < 𝑦𝐼 < 𝑗))
198 fveq2 6907 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑗 → (𝑌𝑦) = (𝑌𝑗))
199198breq2d 5160 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑗 → ((𝑌𝐼) < (𝑌𝑦) ↔ (𝑌𝐼) < (𝑌𝑗)))
200197, 199imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌𝐼) < (𝑌𝑦)) ↔ (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗))))
201196, 200rspc2v 3633 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗))))
202191, 192, 201syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗))))
203190, 202mpd 15 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗)))
204203syldbl2 841 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) < (𝑌𝑗))
205183, 185, 186, 187, 204lttrd 11420 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) < (𝑌𝑗))
206183, 205ltned 11395 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) ≠ (𝑌𝑗))
207206necomd 2994 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝑗) ≠ (𝑋𝐼))
208174, 181, 2073jaodan 1430 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗)) → (𝑌𝑗) ≠ (𝑋𝐼))
209105, 208mpdan 687 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ≠ (𝑋𝐼))
2102093expa 1117 . . . . . . 7 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ≠ (𝑋𝐼))
211210neneqd 2943 . . . . . 6 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌𝑗) = (𝑋𝐼))
212211ralrimiva 3144 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼))
213 ralnex 3070 . . . . . . . 8 (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼))
214213a1i 11 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
215 nnel 3054 . . . . . . . . . 10 (¬ (𝑋𝐼) ∉ ran 𝑌 ↔ (𝑋𝐼) ∈ ran 𝑌)
216215a1i 11 . . . . . . . . 9 (𝜑 → (¬ (𝑋𝐼) ∉ ran 𝑌 ↔ (𝑋𝐼) ∈ ran 𝑌))
217 fvelrnb 6969 . . . . . . . . . 10 (𝑌 Fn (1...𝐾) → ((𝑋𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
21846, 217syl 17 . . . . . . . . 9 (𝜑 → ((𝑋𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
219216, 218bitrd 279 . . . . . . . 8 (𝜑 → (¬ (𝑋𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
220219con1bid 355 . . . . . . 7 (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼) ↔ (𝑋𝐼) ∉ ran 𝑌))
221214, 220bitrd 279 . . . . . 6 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ (𝑋𝐼) ∉ ran 𝑌))
222221adantr 480 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ (𝑋𝐼) ∉ ran 𝑌))
223212, 222mpbid 232 . . . 4 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → (𝑋𝐼) ∉ ran 𝑌)
224 elnelne1 3055 . . . 4 (((𝑋𝐼) ∈ ran 𝑋 ∧ (𝑋𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌)
22599, 223, 224syl2anc 584 . . 3 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → ran 𝑋 ≠ ran 𝑌)
22645ffund 6741 . . . . . 6 (𝜑 → Fun 𝑌)
227226adantr 480 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → Fun 𝑌)
22845fdmd 6747 . . . . . . 7 (𝜑 → dom 𝑌 = (1...𝐾))
22970, 228eleqtrrd 2842 . . . . . 6 (𝜑𝐼 ∈ dom 𝑌)
230229adantr 480 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → 𝐼 ∈ dom 𝑌)
231 fvelrn 7096 . . . . 5 ((Fun 𝑌𝐼 ∈ dom 𝑌) → (𝑌𝐼) ∈ ran 𝑌)
232227, 230, 231syl2anc 584 . . . 4 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → (𝑌𝐼) ∈ ran 𝑌)
2331003ad2ant3 1134 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
234233nnred 12279 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
2351033ad2ant1 1132 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
236234, 235lttri4d 11400 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗))
237313ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁))
238 simp3 1137 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
239237, 238ffvelcdmd 7105 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ∈ (1...𝑁))
240109sseli 3991 . . . . . . . . . . . . . 14 ((𝑋𝑗) ∈ (1...𝑁) → (𝑋𝑗) ∈ ℕ)
241239, 240syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ∈ ℕ)
242241nnred 12279 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ∈ ℝ)
243242adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) ∈ ℝ)
2441883ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
245244adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
246 simpl3 1192 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
247703ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
248247adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
249 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑗 → (𝑌𝑥) = (𝑌𝑗))
250249breq1d 5158 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑗 → ((𝑌𝑥) < (𝑌𝑦) ↔ (𝑌𝑗) < (𝑌𝑦)))
251121, 250imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) ↔ (𝑗 < 𝑦 → (𝑌𝑗) < (𝑌𝑦))))
252 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝐼 → (𝑌𝑦) = (𝑌𝐼))
253252breq2d 5160 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐼 → ((𝑌𝑗) < (𝑌𝑦) ↔ (𝑌𝑗) < (𝑌𝐼)))
254125, 253imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌𝑗) < (𝑌𝑦)) ↔ (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼))))
255251, 254rspc2v 3633 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼))))
256246, 248, 255syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼))))
257245, 256mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼)))
258257syldbl2 841 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) < (𝑌𝐼))
2591693adantl2 1166 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
260259breq1d 5158 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋𝑗) < (𝑌𝐼) ↔ (𝑌𝑗) < (𝑌𝐼)))
261258, 260mpbird 257 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) < (𝑌𝐼))
262243, 261ltned 11395 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) ≠ (𝑌𝐼))
263893ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝐼) ∈ ℝ)
264263adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) ∈ ℝ)
265 simpl2 1191 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) < (𝑋𝐼))
266264, 265ltned 11395 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) ≠ (𝑋𝐼))
267266necomd 2994 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋𝐼) ≠ (𝑌𝐼))
268 fveq2 6907 . . . . . . . . . . . . 13 (𝑗 = 𝐼 → (𝑋𝑗) = (𝑋𝐼))
269268neeq1d 2998 . . . . . . . . . . . 12 (𝑗 = 𝐼 → ((𝑋𝑗) ≠ (𝑌𝐼) ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
270269adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋𝑗) ≠ (𝑌𝐼) ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
271267, 270mpbird 257 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋𝑗) ≠ (𝑌𝐼))
272263adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) ∈ ℝ)
273873ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝐼) ∈ ℝ)
274273adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) ∈ ℝ)
275242adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝑗) ∈ ℝ)
276 simpl2 1191 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) < (𝑋𝐼))
2771153ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
278277adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
279247adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
280238adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
281 fveq2 6907 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝐼 → (𝑋𝑥) = (𝑋𝐼))
282281breq1d 5158 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐼 → ((𝑋𝑥) < (𝑋𝑦) ↔ (𝑋𝐼) < (𝑋𝑦)))
283193, 282imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) ↔ (𝐼 < 𝑦 → (𝑋𝐼) < (𝑋𝑦))))
284 fveq2 6907 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑗 → (𝑋𝑦) = (𝑋𝑗))
285284breq2d 5160 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑗 → ((𝑋𝐼) < (𝑋𝑦) ↔ (𝑋𝐼) < (𝑋𝑗)))
286197, 285imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋𝐼) < (𝑋𝑦)) ↔ (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗))))
287283, 286rspc2v 3633 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗))))
288279, 280, 287syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗))))
289278, 288mpd 15 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗)))
290289syldbl2 841 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) < (𝑋𝑗))
291272, 274, 275, 276, 290lttrd 11420 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) < (𝑋𝑗))
292272, 291ltned 11395 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) ≠ (𝑋𝑗))
293292necomd 2994 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝑗) ≠ (𝑌𝐼))
294262, 271, 2933jaodan 1430 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗)) → (𝑋𝑗) ≠ (𝑌𝐼))
295236, 294mpdan 687 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ≠ (𝑌𝐼))
2962953expa 1117 . . . . . . 7 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ≠ (𝑌𝐼))
297296neneqd 2943 . . . . . 6 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋𝑗) = (𝑌𝐼))
298297ralrimiva 3144 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼))
299 ralnex 3070 . . . . . . . 8 (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼))
300299a1i 11 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
301 nnel 3054 . . . . . . . . . 10 (¬ (𝑌𝐼) ∉ ran 𝑋 ↔ (𝑌𝐼) ∈ ran 𝑋)
302301a1i 11 . . . . . . . . 9 (𝜑 → (¬ (𝑌𝐼) ∉ ran 𝑋 ↔ (𝑌𝐼) ∈ ran 𝑋))
303 fvelrnb 6969 . . . . . . . . . 10 (𝑋 Fn (1...𝐾) → ((𝑌𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
30432, 303syl 17 . . . . . . . . 9 (𝜑 → ((𝑌𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
305302, 304bitrd 279 . . . . . . . 8 (𝜑 → (¬ (𝑌𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
306305con1bid 355 . . . . . . 7 (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼) ↔ (𝑌𝐼) ∉ ran 𝑋))
307300, 306bitrd 279 . . . . . 6 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ (𝑌𝐼) ∉ ran 𝑋))
308307adantr 480 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ (𝑌𝐼) ∉ ran 𝑋))
309298, 308mpbid 232 . . . 4 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → (𝑌𝐼) ∉ ran 𝑋)
310 elnelne1 3055 . . . . 5 (((𝑌𝐼) ∈ ran 𝑌 ∧ (𝑌𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋)
311310necomd 2994 . . . 4 (((𝑌𝐼) ∈ ran 𝑌 ∧ (𝑌𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌)
312232, 309, 311syl2anc 584 . . 3 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → ran 𝑋 ≠ ran 𝑌)
313225, 312jaodan 959 . 2 ((𝜑 ∧ ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼))) → ran 𝑋 ≠ ran 𝑌)
31492, 313mpdan 687 1 (𝜑 → ran 𝑋 ≠ ran 𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3o 1085  w3a 1086  wal 1535   = wceq 1537  wcel 2106  {cab 2712  wne 2938  wnel 3044  wral 3059  wrex 3068  {crab 3433  wss 3963  c0 4339   class class class wbr 5148   Or wor 5596  dom cdm 5689  ran crn 5690  Fun wfun 6557   Fn wfn 6558  wf 6559  cfv 6563  (class class class)co 7431  Fincfn 8984  infcinf 9479  cr 11152  1c1 11154   < clt 11293  cle 11294  cn 12264  0cn0 12524  ...cfz 13544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612  df-uz 12877  df-fz 13545
This theorem is referenced by:  sticksstones2  42129
  Copyright terms: Public domain W3C validator