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 39859
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 10938 . . . . . . 7 < Or ℝ
43a1i 11 . . . . . 6 (𝜑 → < Or ℝ)
5 fzfid 13573 . . . . . . . 8 (𝜑 → (1...𝐾) ∈ Fin)
6 ssrab2 4008 . . . . . . . . 9 {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ (1...𝐾)
76a1i 11 . . . . . . . 8 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ (1...𝐾))
8 ssfi 8874 . . . . . . . 8 (((1...𝐾) ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin)
95, 7, 8syl2anc 587 . . . . . . 7 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin)
10 sticksstones1.6 . . . . . . . 8 (𝜑𝑋𝑌)
11 rabeq0 4314 . . . . . . . . . . . . 13 ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋𝑧) ≠ (𝑌𝑧))
12 nne 2945 . . . . . . . . . . . . . 14 (¬ (𝑋𝑧) ≠ (𝑌𝑧) ↔ (𝑋𝑧) = (𝑌𝑧))
1312ralbii 3089 . . . . . . . . . . . . 13 (∀𝑧 ∈ (1...𝐾) ¬ (𝑋𝑧) ≠ (𝑌𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧))
1411, 13bitri 278 . . . . . . . . . . . 12 ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧))
15 feq1 6545 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁)))
16 fveq1 6735 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑋 → (𝑓𝑥) = (𝑋𝑥))
17 fveq1 6735 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑋 → (𝑓𝑦) = (𝑋𝑦))
1816, 17breq12d 5081 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑋 → ((𝑓𝑥) < (𝑓𝑦) ↔ (𝑋𝑥) < (𝑋𝑦)))
1918imbi2d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ (𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦))))
20192ralbidv 3121 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝑋 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦))))
2115, 20anbi12d 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...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))))
2422, 23mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓(𝑓𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2524spi 2182 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2625biimpi 219 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝐴 → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2726adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓𝐴) → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
2827ralrimiva 3106 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑓𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))))
29 sticksstones1.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑋𝐴)
3021, 28, 29rspcdva 3552 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦))))
3130simpld 498 . . . . . . . . . . . . . . . . . 18 (𝜑𝑋:(1...𝐾)⟶(1...𝑁))
3231ffnd 6565 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 Fn (1...𝐾))
3332adantr 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 (𝑓 = 𝑌 → (𝑓𝑦) = (𝑌𝑦))
3836, 37breq12d 5081 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑌 → ((𝑓𝑥) < (𝑓𝑦) ↔ (𝑌𝑥) < (𝑌𝑦)))
3938imbi2d 344 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ (𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
40392ralbidv 3121 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4135, 40anbi12d 634 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))))
4241, 28, 34rspcdva 3552 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4342adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑌𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4434, 43mpdan 687 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦))))
4544simpld 498 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌:(1...𝐾)⟶(1...𝑁))
4645ffnd 6565 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 Fn (1...𝐾))
4746adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → 𝑌 Fn (1...𝐾))
48 eqfnfv 6871 . . . . . . . . . . . . . . . 16 ((𝑋 Fn (1...𝐾) ∧ 𝑌 Fn (1...𝐾)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)))
4933, 47, 48syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)))
5049bicomd 226 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧) ↔ 𝑋 = 𝑌))
5150biimpd 232 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧) → 𝑋 = 𝑌))
5251syldbl2 841 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋𝑧) = (𝑌𝑧)) → 𝑋 = 𝑌)
5314, 52sylan2b 597 . . . . . . . . . . 11 ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅) → 𝑋 = 𝑌)
5453ex 416 . . . . . . . . . 10 (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} = ∅ → 𝑋 = 𝑌))
5554necon3d 2962 . . . . . . . . 9 (𝜑 → (𝑋𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅))
5655imp 410 . . . . . . . 8 ((𝜑𝑋𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅)
5710, 56mpdan 687 . . . . . . 7 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅)
58 fz1ssnn 13168 . . . . . . . . . 10 (1...𝐾) ⊆ ℕ
5958a1i 11 . . . . . . . . 9 (𝜑 → (1...𝐾) ⊆ ℕ)
60 nnssre 11859 . . . . . . . . . 10 ℕ ⊆ ℝ
6160a1i 11 . . . . . . . . 9 (𝜑 → ℕ ⊆ ℝ)
6259, 61sstrd 3926 . . . . . . . 8 (𝜑 → (1...𝐾) ⊆ ℝ)
637, 62sstrd 3926 . . . . . . 7 (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ)
649, 57, 633jca 1130 . . . . . 6 (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ))
65 fiinfcl 9142 . . . . . 6 (( < Or ℝ ∧ ({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)})
664, 64, 65syl2anc 587 . . . . 5 (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)})
672, 66eqeltrd 2839 . . . 4 (𝜑𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)})
687, 66sseldd 3917 . . . . . 6 (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ (1...𝐾))
692eleq1d 2823 . . . . . 6 (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ∈ (1...𝐾)))
7068, 69mpbird 260 . . . . 5 (𝜑𝐼 ∈ (1...𝐾))
71 fveq2 6736 . . . . . . 7 (𝑧 = 𝐼 → (𝑋𝑧) = (𝑋𝐼))
72 fveq2 6736 . . . . . . 7 (𝑧 = 𝐼 → (𝑌𝑧) = (𝑌𝐼))
7371, 72neeq12d 3003 . . . . . 6 (𝑧 = 𝐼 → ((𝑋𝑧) ≠ (𝑌𝑧) ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
7473elrab3 3616 . . . . 5 (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
7570, 74syl 17 . . . 4 (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
7667, 75mpbid 235 . . 3 (𝜑 → (𝑋𝐼) ≠ (𝑌𝐼))
77 nfv 1922 . . . . . 6 𝑎𝜑
78 nfcv 2905 . . . . . 6 𝑎(1...𝑁)
79 nfcv 2905 . . . . . 6 𝑎
80 elfznn 13166 . . . . . . . . 9 (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
8180adantl 485 . . . . . . . 8 ((𝜑𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ)
82 nnre 11862 . . . . . . . 8 (𝑎 ∈ ℕ → 𝑎 ∈ ℝ)
8381, 82syl 17 . . . . . . 7 ((𝜑𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ)
8483ex 416 . . . . . 6 (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ))
8577, 78, 79, 84ssrd 3921 . . . . 5 (𝜑 → (1...𝑁) ⊆ ℝ)
8631, 70ffvelrnd 6924 . . . . 5 (𝜑 → (𝑋𝐼) ∈ (1...𝑁))
8785, 86sseldd 3917 . . . 4 (𝜑 → (𝑋𝐼) ∈ ℝ)
8845, 70ffvelrnd 6924 . . . . 5 (𝜑 → (𝑌𝐼) ∈ (1...𝑁))
8985, 88sseldd 3917 . . . 4 (𝜑 → (𝑌𝐼) ∈ ℝ)
90 lttri2 10940 . . . 4 (((𝑋𝐼) ∈ ℝ ∧ (𝑌𝐼) ∈ ℝ) → ((𝑋𝐼) ≠ (𝑌𝐼) ↔ ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼))))
9187, 89, 90syl2anc 587 . . 3 (𝜑 → ((𝑋𝐼) ≠ (𝑌𝐼) ↔ ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼))))
9276, 91mpbid 235 . 2 (𝜑 → ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼)))
9331ffund 6568 . . . . . 6 (𝜑 → Fun 𝑋)
9493adantr 484 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → Fun 𝑋)
9531fdmd 6575 . . . . . . 7 (𝜑 → dom 𝑋 = (1...𝐾))
9670, 95eleqtrrd 2842 . . . . . 6 (𝜑𝐼 ∈ dom 𝑋)
9796adantr 484 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → 𝐼 ∈ dom 𝑋)
98 fvelrn 6916 . . . . 5 ((Fun 𝑋𝐼 ∈ dom 𝑋) → (𝑋𝐼) ∈ ran 𝑋)
9994, 97, 98syl2anc 587 . . . 4 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → (𝑋𝐼) ∈ ran 𝑋)
100 elfznn 13166 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ)
1011003ad2ant3 1137 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
102101nnred 11870 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
10362, 70sseldd 3917 . . . . . . . . . . 11 (𝜑𝐼 ∈ ℝ)
1041033ad2ant1 1135 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
105102, 104lttri4d 10998 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗))
106453ad2ant1 1135 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁))
107 simp3 1140 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
108106, 107ffvelrnd 6924 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ∈ (1...𝑁))
109 fz1ssnn 13168 . . . . . . . . . . . . . . 15 (1...𝑁) ⊆ ℕ
110109sseli 3911 . . . . . . . . . . . . . 14 ((𝑌𝑗) ∈ (1...𝑁) → (𝑌𝑗) ∈ ℕ)
111 nnre 11862 . . . . . . . . . . . . . 14 ((𝑌𝑗) ∈ ℕ → (𝑌𝑗) ∈ ℝ)
112110, 111syl 17 . . . . . . . . . . . . 13 ((𝑌𝑗) ∈ (1...𝑁) → (𝑌𝑗) ∈ ℝ)
113108, 112syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ∈ ℝ)
114113adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) ∈ ℝ)
11530simprd 499 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
1161153ad2ant1 1135 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
117116adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
118 simpl3 1195 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
119703ad2ant1 1135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
120119adantr 484 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
121 breq1 5071 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑗 → (𝑥 < 𝑦𝑗 < 𝑦))
122 fveq2 6736 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑗 → (𝑋𝑥) = (𝑋𝑗))
123122breq1d 5078 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑗 → ((𝑋𝑥) < (𝑋𝑦) ↔ (𝑋𝑗) < (𝑋𝑦)))
124121, 123imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) ↔ (𝑗 < 𝑦 → (𝑋𝑗) < (𝑋𝑦))))
125 breq2 5072 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐼 → (𝑗 < 𝑦𝑗 < 𝐼))
126 fveq2 6736 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝐼 → (𝑋𝑦) = (𝑋𝐼))
127126breq2d 5080 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐼 → ((𝑋𝑗) < (𝑋𝑦) ↔ (𝑋𝑗) < (𝑋𝐼)))
128125, 127imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋𝑗) < (𝑋𝑦)) ↔ (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼))))
129124, 128rspc2v 3560 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼))))
130118, 120, 129syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼))))
131117, 130mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑋𝑗) < (𝑋𝐼)))
132131syldbl2 841 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) < (𝑋𝐼))
133 simp2 1139 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
134 simp3 1140 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼)
1351003ad2ant2 1136 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ)
136135nnred 11870 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ)
1371033ad2ant1 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ)
138136, 137ltnled 11004 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼𝑗))
139134, 138mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼𝑗)
140633ad2ant1 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ)
14193ad2ant1 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin)
142 infrefilb 11843 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗)
1431423expia 1123 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ∈ Fin) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗))
144140, 141, 143syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗))
145144imp 410 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗)
1461a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ))
147146breq1d 5078 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → (𝐼𝑗 ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}, ℝ, < ) ≤ 𝑗))
148145, 147mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}) → 𝐼𝑗)
149148ex 416 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} → 𝐼𝑗))
150149con3d 155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝐼𝑗 → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)}))
151139, 150mpd 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 (𝑧 = 𝑗 → (𝑌𝑧) = (𝑌𝑗))
157155, 156neeq12d 3003 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑗 → ((𝑋𝑧) ≠ (𝑌𝑧) ↔ (𝑋𝑗) ≠ (𝑌𝑗)))
158152, 153, 154, 157elrabf 3611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋𝑗) ≠ (𝑌𝑗)))
159158notbii 323 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋𝑗) ≠ (𝑌𝑗)))
160 ianor 982 . . . . . . . . . . . . . . . . . . . . . 22 (¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋𝑗) ≠ (𝑌𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
161159, 160bitri 278 . . . . . . . . . . . . . . . . . . . . 21 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋𝑧) ≠ (𝑌𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
162151, 161sylib 221 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
163 imor 853 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ (1...𝐾) → ¬ (𝑋𝑗) ≠ (𝑌𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
164162, 163sylibr 237 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋𝑗) ≠ (𝑌𝑗)))
165164imp 410 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋𝑗) ≠ (𝑌𝑗))
166 nne 2945 . . . . . . . . . . . . . . . . . 18 (¬ (𝑋𝑗) ≠ (𝑌𝑗) ↔ (𝑋𝑗) = (𝑌𝑗))
167165, 166sylib 221 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) = (𝑌𝑗))
168133, 167mpdan 687 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
1691683expa 1120 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
1701693adantl2 1169 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
171170eqcomd 2744 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) = (𝑋𝑗))
172171breq1d 5078 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌𝑗) < (𝑋𝐼) ↔ (𝑋𝑗) < (𝑋𝐼)))
173132, 172mpbird 260 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) < (𝑋𝐼))
174114, 173ltned 10993 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) ≠ (𝑋𝐼))
175763ad2ant1 1135 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝐼) ≠ (𝑌𝐼))
176175adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋𝐼) ≠ (𝑌𝐼))
177176necomd 2997 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) ≠ (𝑋𝐼))
178 fveq2 6736 . . . . . . . . . . . . 13 (𝑗 = 𝐼 → (𝑌𝑗) = (𝑌𝐼))
179178neeq1d 3001 . . . . . . . . . . . 12 (𝑗 = 𝐼 → ((𝑌𝑗) ≠ (𝑋𝐼) ↔ (𝑌𝐼) ≠ (𝑋𝐼)))
180179adantl 485 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌𝑗) ≠ (𝑋𝐼) ↔ (𝑌𝐼) ≠ (𝑋𝐼)))
181177, 180mpbird 260 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝑗) ≠ (𝑋𝐼))
182873ad2ant1 1135 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝐼) ∈ ℝ)
183182adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) ∈ ℝ)
184893ad2ant1 1135 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝐼) ∈ ℝ)
185184adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) ∈ ℝ)
186113adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝑗) ∈ ℝ)
187 simpl2 1194 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) < (𝑌𝐼))
18842simprd 499 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
1891883ad2ant1 1135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
190189adantr 484 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
191119adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
192107adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
193 breq1 5071 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐼 → (𝑥 < 𝑦𝐼 < 𝑦))
194 fveq2 6736 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝐼 → (𝑌𝑥) = (𝑌𝐼))
195194breq1d 5078 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐼 → ((𝑌𝑥) < (𝑌𝑦) ↔ (𝑌𝐼) < (𝑌𝑦)))
196193, 195imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) ↔ (𝐼 < 𝑦 → (𝑌𝐼) < (𝑌𝑦))))
197 breq2 5072 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑗 → (𝐼 < 𝑦𝐼 < 𝑗))
198 fveq2 6736 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑗 → (𝑌𝑦) = (𝑌𝑗))
199198breq2d 5080 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑗 → ((𝑌𝐼) < (𝑌𝑦) ↔ (𝑌𝐼) < (𝑌𝑗)))
200197, 199imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌𝐼) < (𝑌𝑦)) ↔ (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗))))
201196, 200rspc2v 3560 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗))))
202191, 192, 201syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗))))
203190, 202mpd 15 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑌𝐼) < (𝑌𝑗)))
204203syldbl2 841 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) < (𝑌𝑗))
205183, 185, 186, 187, 204lttrd 11018 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) < (𝑌𝑗))
206183, 205ltned 10993 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) ≠ (𝑌𝑗))
207206necomd 2997 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝑗) ≠ (𝑋𝐼))
208174, 181, 2073jaodan 1432 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗)) → (𝑌𝑗) ≠ (𝑋𝐼))
209105, 208mpdan 687 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ≠ (𝑋𝐼))
2102093expa 1120 . . . . . . 7 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝑗) ≠ (𝑋𝐼))
211210neneqd 2946 . . . . . 6 (((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌𝑗) = (𝑋𝐼))
212211ralrimiva 3106 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼))
213 ralnex 3162 . . . . . . . 8 (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼))
214213a1i 11 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
215 nnel 3056 . . . . . . . . . 10 (¬ (𝑋𝐼) ∉ ran 𝑌 ↔ (𝑋𝐼) ∈ ran 𝑌)
216215a1i 11 . . . . . . . . 9 (𝜑 → (¬ (𝑋𝐼) ∉ ran 𝑌 ↔ (𝑋𝐼) ∈ ran 𝑌))
217 fvelrnb 6792 . . . . . . . . . 10 (𝑌 Fn (1...𝐾) → ((𝑋𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
21846, 217syl 17 . . . . . . . . 9 (𝜑 → ((𝑋𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
219216, 218bitrd 282 . . . . . . . 8 (𝜑 → (¬ (𝑋𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼)))
220219con1bid 359 . . . . . . 7 (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑌𝑗) = (𝑋𝐼) ↔ (𝑋𝐼) ∉ ran 𝑌))
221214, 220bitrd 282 . . . . . 6 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ (𝑋𝐼) ∉ ran 𝑌))
222221adantr 484 . . . . 5 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌𝑗) = (𝑋𝐼) ↔ (𝑋𝐼) ∉ ran 𝑌))
223212, 222mpbid 235 . . . 4 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → (𝑋𝐼) ∉ ran 𝑌)
224 elnelne1 3057 . . . 4 (((𝑋𝐼) ∈ ran 𝑋 ∧ (𝑋𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌)
22599, 223, 224syl2anc 587 . . 3 ((𝜑 ∧ (𝑋𝐼) < (𝑌𝐼)) → ran 𝑋 ≠ ran 𝑌)
22645ffund 6568 . . . . . 6 (𝜑 → Fun 𝑌)
227226adantr 484 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → Fun 𝑌)
22845fdmd 6575 . . . . . . 7 (𝜑 → dom 𝑌 = (1...𝐾))
22970, 228eleqtrrd 2842 . . . . . 6 (𝜑𝐼 ∈ dom 𝑌)
230229adantr 484 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → 𝐼 ∈ dom 𝑌)
231 fvelrn 6916 . . . . 5 ((Fun 𝑌𝐼 ∈ dom 𝑌) → (𝑌𝐼) ∈ ran 𝑌)
232227, 230, 231syl2anc 587 . . . 4 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → (𝑌𝐼) ∈ ran 𝑌)
2331003ad2ant3 1137 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
234233nnred 11870 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
2351033ad2ant1 1135 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
236234, 235lttri4d 10998 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗))
237313ad2ant1 1135 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁))
238 simp3 1140 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
239237, 238ffvelrnd 6924 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ∈ (1...𝑁))
240109sseli 3911 . . . . . . . . . . . . . 14 ((𝑋𝑗) ∈ (1...𝑁) → (𝑋𝑗) ∈ ℕ)
241239, 240syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ∈ ℕ)
242241nnred 11870 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ∈ ℝ)
243242adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) ∈ ℝ)
2441883ad2ant1 1135 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
245244adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)))
246 simpl3 1195 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
247703ad2ant1 1135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
248247adantr 484 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
249 fveq2 6736 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑗 → (𝑌𝑥) = (𝑌𝑗))
250249breq1d 5078 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑗 → ((𝑌𝑥) < (𝑌𝑦) ↔ (𝑌𝑗) < (𝑌𝑦)))
251121, 250imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) ↔ (𝑗 < 𝑦 → (𝑌𝑗) < (𝑌𝑦))))
252 fveq2 6736 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝐼 → (𝑌𝑦) = (𝑌𝐼))
253252breq2d 5080 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐼 → ((𝑌𝑗) < (𝑌𝑦) ↔ (𝑌𝑗) < (𝑌𝐼)))
254125, 253imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌𝑗) < (𝑌𝑦)) ↔ (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼))))
255251, 254rspc2v 3560 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼))))
256246, 248, 255syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌𝑥) < (𝑌𝑦)) → (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼))))
257245, 256mpd 15 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑌𝑗) < (𝑌𝐼)))
258257syldbl2 841 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌𝑗) < (𝑌𝐼))
2591693adantl2 1169 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) = (𝑌𝑗))
260259breq1d 5078 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋𝑗) < (𝑌𝐼) ↔ (𝑌𝑗) < (𝑌𝐼)))
261258, 260mpbird 260 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) < (𝑌𝐼))
262243, 261ltned 10993 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋𝑗) ≠ (𝑌𝐼))
263893ad2ant1 1135 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌𝐼) ∈ ℝ)
264263adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) ∈ ℝ)
265 simpl2 1194 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) < (𝑋𝐼))
266264, 265ltned 10993 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌𝐼) ≠ (𝑋𝐼))
267266necomd 2997 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋𝐼) ≠ (𝑌𝐼))
268 fveq2 6736 . . . . . . . . . . . . 13 (𝑗 = 𝐼 → (𝑋𝑗) = (𝑋𝐼))
269268neeq1d 3001 . . . . . . . . . . . 12 (𝑗 = 𝐼 → ((𝑋𝑗) ≠ (𝑌𝐼) ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
270269adantl 485 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋𝑗) ≠ (𝑌𝐼) ↔ (𝑋𝐼) ≠ (𝑌𝐼)))
271267, 270mpbird 260 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋𝑗) ≠ (𝑌𝐼))
272263adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) ∈ ℝ)
273873ad2ant1 1135 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝐼) ∈ ℝ)
274273adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) ∈ ℝ)
275242adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝑗) ∈ ℝ)
276 simpl2 1194 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) < (𝑋𝐼))
2771153ad2ant1 1135 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
278277adantr 484 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)))
279247adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
280238adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
281 fveq2 6736 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝐼 → (𝑋𝑥) = (𝑋𝐼))
282281breq1d 5078 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝐼 → ((𝑋𝑥) < (𝑋𝑦) ↔ (𝑋𝐼) < (𝑋𝑦)))
283193, 282imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) ↔ (𝐼 < 𝑦 → (𝑋𝐼) < (𝑋𝑦))))
284 fveq2 6736 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑗 → (𝑋𝑦) = (𝑋𝑗))
285284breq2d 5080 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑗 → ((𝑋𝐼) < (𝑋𝑦) ↔ (𝑋𝐼) < (𝑋𝑗)))
286197, 285imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋𝐼) < (𝑋𝑦)) ↔ (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗))))
287283, 286rspc2v 3560 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗))))
288279, 280, 287syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋𝑥) < (𝑋𝑦)) → (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗))))
289278, 288mpd 15 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑋𝐼) < (𝑋𝑗)))
290289syldbl2 841 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝐼) < (𝑋𝑗))
291272, 274, 275, 276, 290lttrd 11018 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) < (𝑋𝑗))
292272, 291ltned 10993 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌𝐼) ≠ (𝑋𝑗))
293292necomd 2997 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋𝑗) ≠ (𝑌𝐼))
294262, 271, 2933jaodan 1432 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼𝑗 = 𝐼𝐼 < 𝑗)) → (𝑋𝑗) ≠ (𝑌𝐼))
295236, 294mpdan 687 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ≠ (𝑌𝐼))
2962953expa 1120 . . . . . . 7 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋𝑗) ≠ (𝑌𝐼))
297296neneqd 2946 . . . . . 6 (((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋𝑗) = (𝑌𝐼))
298297ralrimiva 3106 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼))
299 ralnex 3162 . . . . . . . 8 (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼))
300299a1i 11 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
301 nnel 3056 . . . . . . . . . 10 (¬ (𝑌𝐼) ∉ ran 𝑋 ↔ (𝑌𝐼) ∈ ran 𝑋)
302301a1i 11 . . . . . . . . 9 (𝜑 → (¬ (𝑌𝐼) ∉ ran 𝑋 ↔ (𝑌𝐼) ∈ ran 𝑋))
303 fvelrnb 6792 . . . . . . . . . 10 (𝑋 Fn (1...𝐾) → ((𝑌𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
30432, 303syl 17 . . . . . . . . 9 (𝜑 → ((𝑌𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
305302, 304bitrd 282 . . . . . . . 8 (𝜑 → (¬ (𝑌𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼)))
306305con1bid 359 . . . . . . 7 (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑋𝑗) = (𝑌𝐼) ↔ (𝑌𝐼) ∉ ran 𝑋))
307300, 306bitrd 282 . . . . . 6 (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ (𝑌𝐼) ∉ ran 𝑋))
308307adantr 484 . . . . 5 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋𝑗) = (𝑌𝐼) ↔ (𝑌𝐼) ∉ ran 𝑋))
309298, 308mpbid 235 . . . 4 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → (𝑌𝐼) ∉ ran 𝑋)
310 elnelne1 3057 . . . . 5 (((𝑌𝐼) ∈ ran 𝑌 ∧ (𝑌𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋)
311310necomd 2997 . . . 4 (((𝑌𝐼) ∈ ran 𝑌 ∧ (𝑌𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌)
312232, 309, 311syl2anc 587 . . 3 ((𝜑 ∧ (𝑌𝐼) < (𝑋𝐼)) → ran 𝑋 ≠ ran 𝑌)
313225, 312jaodan 958 . 2 ((𝜑 ∧ ((𝑋𝐼) < (𝑌𝐼) ∨ (𝑌𝐼) < (𝑋𝐼))) → ran 𝑋 ≠ ran 𝑌)
31492, 313mpdan 687 1 (𝜑 → ran 𝑋 ≠ ran 𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3o 1088  w3a 1089  wal 1541   = wceq 1543  wcel 2111  {cab 2715  wne 2941  wnel 3047  wral 3062  wrex 3063  {crab 3066  wss 3881  c0 4252   class class class wbr 5068   Or wor 5482  dom cdm 5566  ran crn 5567  Fun wfun 6392   Fn wfn 6393  wf 6394  cfv 6398  (class class class)co 7232  Fincfn 8647  infcinf 9082  cr 10753  1c1 10755   < clt 10892  cle 10893  cn 11855  0cn0 12115  ...cfz 13120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5207  ax-nul 5214  ax-pow 5273  ax-pr 5337  ax-un 7542  ax-cnex 10810  ax-resscn 10811  ax-1cn 10812  ax-icn 10813  ax-addcl 10814  ax-addrcl 10815  ax-mulcl 10816  ax-mulrcl 10817  ax-mulcom 10818  ax-addass 10819  ax-mulass 10820  ax-distr 10821  ax-i2m1 10822  ax-1ne0 10823  ax-1rid 10824  ax-rnegex 10825  ax-rrecex 10826  ax-cnre 10827  ax-pre-lttri 10828  ax-pre-lttrn 10829  ax-pre-ltadd 10830  ax-pre-mulgt0 10831  ax-pre-sup 10832
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4253  df-if 4455  df-pw 4530  df-sn 4557  df-pr 4559  df-tp 4561  df-op 4563  df-uni 4835  df-iun 4921  df-br 5069  df-opab 5131  df-mpt 5151  df-tr 5177  df-id 5470  df-eprel 5475  df-po 5483  df-so 5484  df-fr 5524  df-we 5526  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-pred 6176  df-ord 6234  df-on 6235  df-lim 6236  df-suc 6237  df-iota 6356  df-fun 6400  df-fn 6401  df-f 6402  df-f1 6403  df-fo 6404  df-f1o 6405  df-fv 6406  df-riota 7189  df-ov 7235  df-oprab 7236  df-mpo 7237  df-om 7664  df-1st 7780  df-2nd 7781  df-wrecs 8068  df-recs 8129  df-rdg 8167  df-1o 8223  df-er 8412  df-en 8648  df-dom 8649  df-sdom 8650  df-fin 8651  df-sup 9083  df-inf 9084  df-pnf 10894  df-mnf 10895  df-xr 10896  df-ltxr 10897  df-le 10898  df-sub 11089  df-neg 11090  df-nn 11856  df-n0 12116  df-z 12202  df-uz 12464  df-fz 13121
This theorem is referenced by:  sticksstones2  39860
  Copyright terms: Public domain W3C validator