sticksstones1 - Mathbox for metakunt

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

Theorem sticksstones1 41054

Description: Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024.)

**Hypotheses**
Ref	Expression
sticksstones1.1	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
sticksstones1.2	⊢ (𝜑 → 𝐾 ∈ ℕ₀)
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.

Step	Hyp	Ref	Expression
1		sticksstones1.7	. . . . . 6 ⊢ 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < )
2	1	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ))
3		ltso 11296	. . . . . . 7 ⊢ < Or ℝ
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
5		fzfid 13940	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
6		ssrab2 4077	. . . . . . . . 9 ⊢ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾))
8		ssfi 9175	. . . . . . . 8 ⊢ (((1...𝐾) ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
9	5, 7, 8	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
10		sticksstones1.6	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11		rabeq0 4384	. . . . . . . . . . . . 13 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧))
12		nne 2944	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑧) = (𝑌‘𝑧))
13	12	ralbii 3093	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
14	11, 13	bitri 274	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
15		feq1 6698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁)))
16		fveq1 6890	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑥) = (𝑋‘𝑥))
17		fveq1 6890	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑦) = (𝑋‘𝑦))
18	16, 17	breq12d 5161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑋 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑋‘𝑥) < (𝑋‘𝑦)))
19	18	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
20	19	2ralbidv 3218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑋 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
21	15, 20	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑋 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))))
22		sticksstones1.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}
23		eqabb 2873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))))
24	22, 23	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
25	24	spi 2177	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
26	25	biimpi 215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ 𝐴 → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
27	26	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
28	27	ralrimiva 3146	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
29		sticksstones1.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
30	21, 28, 29	rspcdva 3613	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
31	30	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋:(1...𝐾)⟶(1...𝑁))
32	31	ffnd 6718	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 Fn (1...𝐾))
33	32	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 Fn (1...𝐾))
34		sticksstones1.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 ∈ 𝐴)
35		feq1 6698	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑌:(1...𝐾)⟶(1...𝑁)))
36		fveq1 6890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑥) = (𝑌‘𝑥))
37		fveq1 6890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑦) = (𝑌‘𝑦))
38	36, 37	breq12d 5161	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑌 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑌‘𝑥) < (𝑌‘𝑦)))
39	38	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
40	39	2ralbidv 3218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
41	35, 40	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))))
42	41, 28, 34	rspcdva 3613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
43	42	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
44	34, 43	mpdan 685	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
45	44	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌:(1...𝐾)⟶(1...𝑁))
46	45	ffnd 6718	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 Fn (1...𝐾))
47	46	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑌 Fn (1...𝐾))
48		eqfnfv 7032	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 Fn (1...𝐾) ∧ 𝑌 Fn (1...𝐾)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)))
49	33, 47, 48	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)))
50	49	bicomd 222	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) ↔ 𝑋 = 𝑌))
51	50	biimpd 228	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) → 𝑋 = 𝑌))
52	51	syldbl2 839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 = 𝑌)
53	14, 52	sylan2b 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅) → 𝑋 = 𝑌)
54	53	ex 413	. . . . . . . . . 10 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ → 𝑋 = 𝑌))
55	54	necon3d 2961	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ≠ 𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅))
56	55	imp 407	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
57	10, 56	mpdan 685	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
58		fz1ssnn 13534	. . . . . . . . . 10 ⊢ (1...𝐾) ⊆ ℕ
59	58	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1...𝐾) ⊆ ℕ)
60		nnssre 12218	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
61	60	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℕ ⊆ ℝ)
62	59, 61	sstrd 3992	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ⊆ ℝ)
63	7, 62	sstrd 3992	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
64	9, 57, 63	3jca 1128	. . . . . 6 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ))
65		fiinfcl 9498	. . . . . 6 ⊢ (( < Or ℝ ∧ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
66	4, 64, 65	syl2anc 584	. . . . 5 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
67	2, 66	eqeltrd 2833	. . . 4 ⊢ (𝜑 → 𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
68	7, 66	sseldd 3983	. . . . . 6 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾))
69	2	eleq1d 2818	. . . . . 6 ⊢ (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾)))
70	68, 69	mpbird 256	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (1...𝐾))
71		fveq2 6891	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑋‘𝑧) = (𝑋‘𝐼))
72		fveq2 6891	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑌‘𝑧) = (𝑌‘𝐼))
73	71, 72	neeq12d 3002	. . . . . 6 ⊢ (𝑧 = 𝐼 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
74	73	elrab3 3684	. . . . 5 ⊢ (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
75	70, 74	syl 17	. . . 4 ⊢ (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
76	67, 75	mpbid 231	. . 3 ⊢ (𝜑 → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
77		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑎𝜑
78		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑎(1...𝑁)
79		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑎ℝ
80		elfznn 13532	. . . . . . . . 9 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
81	80	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ)
82		nnre 12221	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℝ)
83	81, 82	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ)
84	83	ex 413	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ))
85	77, 78, 79, 84	ssrd 3987	. . . . 5 ⊢ (𝜑 → (1...𝑁) ⊆ ℝ)
86	31, 70	ffvelcdmd 7087	. . . . 5 ⊢ (𝜑 → (𝑋‘𝐼) ∈ (1...𝑁))
87	85, 86	sseldd 3983	. . . 4 ⊢ (𝜑 → (𝑋‘𝐼) ∈ ℝ)
88	45, 70	ffvelcdmd 7087	. . . . 5 ⊢ (𝜑 → (𝑌‘𝐼) ∈ (1...𝑁))
89	85, 88	sseldd 3983	. . . 4 ⊢ (𝜑 → (𝑌‘𝐼) ∈ ℝ)
90		lttri2 11298	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ℝ ∧ (𝑌‘𝐼) ∈ ℝ) → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
91	87, 89, 90	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
92	76, 91	mpbid 231	. 2 ⊢ (𝜑 → ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))
93	31	ffund 6721	. . . . . 6 ⊢ (𝜑 → Fun 𝑋)
94	93	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → Fun 𝑋)
95	31	fdmd 6728	. . . . . . 7 ⊢ (𝜑 → dom 𝑋 = (1...𝐾))
96	70, 95	eleqtrrd 2836	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑋)
97	96	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → 𝐼 ∈ dom 𝑋)
98		fvelrn 7078	. . . . 5 ⊢ ((Fun 𝑋 ∧ 𝐼 ∈ dom 𝑋) → (𝑋‘𝐼) ∈ ran 𝑋)
99	94, 97, 98	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∈ ran 𝑋)
100		elfznn 13532	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ)
101	100	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
102	101	nnred 12229	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
103	62, 70	sseldd 3983	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
104	103	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
105	102, 104	lttri4d 11357	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
106	45	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁))
107		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
108	106, 107	ffvelcdmd 7087	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ (1...𝑁))
109		fz1ssnn 13534	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
110	109	sseli 3978	. . . . . . . . . . . . . 14 ⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℕ)
111		nnre 12221	. . . . . . . . . . . . . 14 ⊢ ((𝑌‘𝑗) ∈ ℕ → (𝑌‘𝑗) ∈ ℝ)
112	110, 111	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℝ)
113	108, 112	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ ℝ)
114	113	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ∈ ℝ)
115	30	simprd 496	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
116	115	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
117	116	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
118		simpl3 1193	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
119	70	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
120	119	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
121		breq1 5151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → (𝑥 < 𝑦 ↔ 𝑗 < 𝑦))
122		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑋‘𝑥) = (𝑋‘𝑗))
123	122	breq1d 5158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝑦)))
124	121, 123	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦))))
125		breq2 5152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → (𝑗 < 𝑦 ↔ 𝑗 < 𝐼))
126		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑋‘𝑦) = (𝑋‘𝐼))
127	126	breq2d 5160	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑋‘𝑗) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
128	125, 127	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
129	124, 128	rspc2v 3622	. . . . . . . . . . . . . . 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 839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑋‘𝐼))
133		simp2 1137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
134		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼)
135	100	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ)
136	135	nnred 12229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ)
137	103	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ)
138	136, 137	ltnled 11363	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼 ≤ 𝑗))
139	134, 138	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼 ≤ 𝑗)
140	63	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
141	9	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
142		infrefilb 12202	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)
146	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ))
147	146	breq1d 5158	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → (𝐼 ≤ 𝑗 ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗))
148	145, 147	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 ≤ 𝑗)
149	148	ex 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → 𝐼 ≤ 𝑗))
150	149	con3d 152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝐼 ≤ 𝑗 → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}))
151	139, 150	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
152		nfcv 2903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧𝑗
153		nfcv 2903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(1...𝐾)
154		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(𝑋‘𝑗) ≠ (𝑌‘𝑗)
155		fveq2 6891	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑋‘𝑧) = (𝑋‘𝑗))
156		fveq2 6891	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑌‘𝑧) = (𝑌‘𝑗))
157	155, 156	neeq12d 3002	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = 𝑗 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
158	152, 153, 154, 157	elrabf 3679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
159	158	notbii 319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
160		ianor 980	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
161	159, 160	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
162	151, 161	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
163		imor 851	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
164	162, 163	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
165	164	imp 407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))
166		nne 2944	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗) ↔ (𝑋‘𝑗) = (𝑌‘𝑗))
167	165, 166	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) = (𝑌‘𝑗))
168	133, 167	mpdan 685	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
169	168	3expa 1118	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
170	169	3adantl2 1167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
171	170	eqcomd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) = (𝑋‘𝑗))
172	171	breq1d 5158	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌‘𝑗) < (𝑋‘𝐼) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
173	132, 172	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑋‘𝐼))
174	114, 173	ltned 11352	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
175	76	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
176	175	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
177	176	necomd 2996	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
178		fveq2 6891	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑌‘𝑗) = (𝑌‘𝐼))
179	178	neeq1d 3000	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
180	179	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
181	177, 180	mpbird 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
182	87	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
183	182	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
184	89	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
185	184	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
186	113	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ∈ ℝ)
187		simpl2 1192	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝐼))
188	42	simprd 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
189	188	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
190	189	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
191	119	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
192	107	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
193		breq1 5151	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → (𝑥 < 𝑦 ↔ 𝐼 < 𝑦))
194		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑌‘𝑥) = (𝑌‘𝐼))
195	194	breq1d 5158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑦)))
196	193, 195	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦))))
197		breq2 5152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → (𝐼 < 𝑦 ↔ 𝐼 < 𝑗))
198		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑌‘𝑦) = (𝑌‘𝑗))
199	198	breq2d 5160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑌‘𝐼) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑗)))
200	197, 199	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
201	196, 200	rspc2v 3622	. . . . . . . . . . . . . . . 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 839	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑌‘𝑗))
205	183, 185, 186, 187, 204	lttrd 11377	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝑗))
206	183, 205	ltned 11352	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ≠ (𝑌‘𝑗))
207	206	necomd 2996	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
208	174, 181, 207	3jaodan 1430	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
209	105, 208	mpdan 685	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
210	209	3expa 1118	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
211	210	neneqd 2945	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
212	211	ralrimiva 3146	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
213		ralnex 3072	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))
214	213	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
215		nnel 3056	. . . . . . . . . 10 ⊢ (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌)
216	215	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌))
217		fvelrnb 6952	. . . . . . . . . 10 ⊢ (𝑌 Fn (1...𝐾) → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
218	46, 217	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
219	216, 218	bitrd 278	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
220	219	con1bid 355	. . . . . . 7 ⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
221	214, 220	bitrd 278	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
222	221	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
223	212, 222	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∉ ran 𝑌)
224		elnelne1 3057	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ran 𝑋 ∧ (𝑋‘𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌)
225	99, 223, 224	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
226	45	ffund 6721	. . . . . 6 ⊢ (𝜑 → Fun 𝑌)
227	226	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → Fun 𝑌)
228	45	fdmd 6728	. . . . . . 7 ⊢ (𝜑 → dom 𝑌 = (1...𝐾))
229	70, 228	eleqtrrd 2836	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑌)
230	229	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → 𝐼 ∈ dom 𝑌)
231		fvelrn 7078	. . . . 5 ⊢ ((Fun 𝑌 ∧ 𝐼 ∈ dom 𝑌) → (𝑌‘𝐼) ∈ ran 𝑌)
232	227, 230, 231	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∈ ran 𝑌)
233	100	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
234	233	nnred 12229	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
235	103	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
236	234, 235	lttri4d 11357	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
237	31	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁))
238		simp3 1138	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
239	237, 238	ffvelcdmd 7087	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ (1...𝑁))
240	109	sseli 3978	. . . . . . . . . . . . . 14 ⊢ ((𝑋‘𝑗) ∈ (1...𝑁) → (𝑋‘𝑗) ∈ ℕ)
241	239, 240	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℕ)
242	241	nnred 12229	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℝ)
243	242	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ∈ ℝ)
244	188	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
245	244	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
246		simpl3 1193	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
247	70	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
248	247	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
249		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑌‘𝑥) = (𝑌‘𝑗))
250	249	breq1d 5158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝑦)))
251	121, 250	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦))))
252		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑌‘𝑦) = (𝑌‘𝐼))
253	252	breq2d 5160	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑌‘𝑗) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
254	125, 253	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
255	251, 254	rspc2v 3622	. . . . . . . . . . . . . . 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 839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑌‘𝐼))
259	169	3adantl2 1167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
260	259	breq1d 5158	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋‘𝑗) < (𝑌‘𝐼) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
261	258, 260	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑌‘𝐼))
262	243, 261	ltned 11352	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
263	89	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
264	263	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ∈ ℝ)
265		simpl2 1192	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) < (𝑋‘𝐼))
266	264, 265	ltned 11352	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
267	266	necomd 2996	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
268		fveq2 6891	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑋‘𝑗) = (𝑋‘𝐼))
269	268	neeq1d 3000	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
270	269	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
271	267, 270	mpbird 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
272	263	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
273	87	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
274	273	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
275	242	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ∈ ℝ)
276		simpl2 1192	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝐼))
277	115	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
278	277	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
279	247	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
280	238	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
281		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑋‘𝑥) = (𝑋‘𝐼))
282	281	breq1d 5158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑦)))
283	193, 282	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦))))
284		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑋‘𝑦) = (𝑋‘𝑗))
285	284	breq2d 5160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑋‘𝐼) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑗)))
286	197, 285	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
287	283, 286	rspc2v 3622	. . . . . . . . . . . . . . . 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 839	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑋‘𝑗))
291	272, 274, 275, 276, 290	lttrd 11377	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝑗))
292	272, 291	ltned 11352	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ≠ (𝑋‘𝑗))
293	292	necomd 2996	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
294	262, 271, 293	3jaodan 1430	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
295	236, 294	mpdan 685	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
296	295	3expa 1118	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
297	296	neneqd 2945	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
298	297	ralrimiva 3146	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
299		ralnex 3072	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))
300	299	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
301		nnel 3056	. . . . . . . . . 10 ⊢ (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋)
302	301	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋))
303		fvelrnb 6952	. . . . . . . . . 10 ⊢ (𝑋 Fn (1...𝐾) → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
304	32, 303	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
305	302, 304	bitrd 278	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
306	305	con1bid 355	. . . . . . 7 ⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
307	300, 306	bitrd 278	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
308	307	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
309	298, 308	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∉ ran 𝑋)
310		elnelne1 3057	. . . . 5 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋)
311	310	necomd 2996	. . . 4 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌)
312	232, 309, 311	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
313	225, 312	jaodan 956	. 2 ⊢ ((𝜑 ∧ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) → ran 𝑋 ≠ ran 𝑌)
314	92, 313	mpdan 685	1 ⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∨ w3o 1086 ∧ w3a 1087 ∀wal 1539 = wceq 1541 ∈ wcel 2106 {cab 2709 ≠ wne 2940 ∉ wnel 3046 ∀wral 3061 ∃wrex 3070 {crab 3432 ⊆ wss 3948 ∅c0 4322 class class class wbr 5148 Or wor 5587 dom cdm 5676 ran crn 5677 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7411 Fincfn 8941 infcinf 9438 ℝcr 11111 1c1 11113 < clt 11250 ≤ cle 11251 ℕcn 12214 ℕ₀cn0 12474 ...cfz 13486

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-inf 9440 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-nn 12215 df-n0 12475 df-z 12561 df-uz 12825 df-fz 13487

This theorem is referenced by: sticksstones2 41055

W3C validator