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 42545

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 11227	. . . . . . 7 ⊢ < Or ℝ
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
5		fzfid 13910	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
6		ssrab2 4034	. . . . . . . . 9 ⊢ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾))
8		ssfi 9111	. . . . . . . 8 ⊢ (((1...𝐾) ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
9	5, 7, 8	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
10		sticksstones1.6	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11		rabeq0 4342	. . . . . . . . . . . . 13 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧))
12		nne 2937	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑧) = (𝑌‘𝑧))
13	12	ralbii 3084	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
14	11, 13	bitri 275	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
15		feq1 6650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁)))
16		fveq1 6843	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑥) = (𝑋‘𝑥))
17		fveq1 6843	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑦) = (𝑋‘𝑦))
18	16, 17	breq12d 5113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑋 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑋‘𝑥) < (𝑋‘𝑦)))
19	18	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
20	19	2ralbidv 3202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑋 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
21	15, 20	anbi12d 633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑋 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))))
22		sticksstones1.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}
23		eqabb 2876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))))
24	22, 23	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
25	24	spi 2192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
26	25	biimpi 216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ 𝐴 → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
27	26	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
28	27	ralrimiva 3130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
29		sticksstones1.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
30	21, 28, 29	rspcdva 3579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
31	30	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋:(1...𝐾)⟶(1...𝑁))
32	31	ffnd 6673	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 Fn (1...𝐾))
33	32	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 Fn (1...𝐾))
34		sticksstones1.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 ∈ 𝐴)
35		feq1 6650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑌:(1...𝐾)⟶(1...𝑁)))
36		fveq1 6843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑥) = (𝑌‘𝑥))
37		fveq1 6843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑦) = (𝑌‘𝑦))
38	36, 37	breq12d 5113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑌 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑌‘𝑥) < (𝑌‘𝑦)))
39	38	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
40	39	2ralbidv 3202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
41	35, 40	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))))
42	41, 28, 34	rspcdva 3579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
43	42	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
44	34, 43	mpdan 688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
45	44	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌:(1...𝐾)⟶(1...𝑁))
46	45	ffnd 6673	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 Fn (1...𝐾))
47	46	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑌 Fn (1...𝐾))
48		eqfnfv 6987	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 Fn (1...𝐾) ∧ 𝑌 Fn (1...𝐾)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)))
49	33, 47, 48	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)))
50	49	bicomd 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) ↔ 𝑋 = 𝑌))
51	50	biimpd 229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) → 𝑋 = 𝑌))
52	51	syldbl2 842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 = 𝑌)
53	14, 52	sylan2b 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅) → 𝑋 = 𝑌)
54	53	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ → 𝑋 = 𝑌))
55	54	necon3d 2954	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ≠ 𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅))
56	55	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
57	10, 56	mpdan 688	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
58		fz1ssnn 13485	. . . . . . . . . 10 ⊢ (1...𝐾) ⊆ ℕ
59	58	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1...𝐾) ⊆ ℕ)
60		nnssre 12163	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
61	60	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℕ ⊆ ℝ)
62	59, 61	sstrd 3946	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ⊆ ℝ)
63	7, 62	sstrd 3946	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
64	9, 57, 63	3jca 1129	. . . . . 6 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ))
65		fiinfcl 9420	. . . . . 6 ⊢ (( < Or ℝ ∧ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
66	4, 64, 65	syl2anc 585	. . . . 5 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
67	2, 66	eqeltrd 2837	. . . 4 ⊢ (𝜑 → 𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
68	7, 66	sseldd 3936	. . . . . 6 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾))
69	2	eleq1d 2822	. . . . . 6 ⊢ (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾)))
70	68, 69	mpbird 257	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (1...𝐾))
71		fveq2 6844	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑋‘𝑧) = (𝑋‘𝐼))
72		fveq2 6844	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑌‘𝑧) = (𝑌‘𝐼))
73	71, 72	neeq12d 2994	. . . . . 6 ⊢ (𝑧 = 𝐼 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
74	73	elrab3 3649	. . . . 5 ⊢ (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
75	70, 74	syl 17	. . . 4 ⊢ (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
76	67, 75	mpbid 232	. . 3 ⊢ (𝜑 → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
77		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑎𝜑
78		nfcv 2899	. . . . . 6 ⊢ Ⅎ𝑎(1...𝑁)
79		nfcv 2899	. . . . . 6 ⊢ Ⅎ𝑎ℝ
80		elfznn 13483	. . . . . . . . 9 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
81	80	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ)
82		nnre 12166	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℝ)
83	81, 82	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ)
84	83	ex 412	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ))
85	77, 78, 79, 84	ssrd 3940	. . . . 5 ⊢ (𝜑 → (1...𝑁) ⊆ ℝ)
86	31, 70	ffvelcdmd 7041	. . . . 5 ⊢ (𝜑 → (𝑋‘𝐼) ∈ (1...𝑁))
87	85, 86	sseldd 3936	. . . 4 ⊢ (𝜑 → (𝑋‘𝐼) ∈ ℝ)
88	45, 70	ffvelcdmd 7041	. . . . 5 ⊢ (𝜑 → (𝑌‘𝐼) ∈ (1...𝑁))
89	85, 88	sseldd 3936	. . . 4 ⊢ (𝜑 → (𝑌‘𝐼) ∈ ℝ)
90		lttri2 11229	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ℝ ∧ (𝑌‘𝐼) ∈ ℝ) → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
91	87, 89, 90	syl2anc 585	. . 3 ⊢ (𝜑 → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
92	76, 91	mpbid 232	. 2 ⊢ (𝜑 → ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))
93	31	ffund 6676	. . . . . 6 ⊢ (𝜑 → Fun 𝑋)
94	93	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → Fun 𝑋)
95	31	fdmd 6682	. . . . . . 7 ⊢ (𝜑 → dom 𝑋 = (1...𝐾))
96	70, 95	eleqtrrd 2840	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑋)
97	96	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → 𝐼 ∈ dom 𝑋)
98		fvelrn 7032	. . . . 5 ⊢ ((Fun 𝑋 ∧ 𝐼 ∈ dom 𝑋) → (𝑋‘𝐼) ∈ ran 𝑋)
99	94, 97, 98	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∈ ran 𝑋)
100		elfznn 13483	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ)
101	100	3ad2ant3 1136	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
102	101	nnred 12174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
103	62, 70	sseldd 3936	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
104	103	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
105	102, 104	lttri4d 11288	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
106	45	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁))
107		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
108	106, 107	ffvelcdmd 7041	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ (1...𝑁))
109		fz1ssnn 13485	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
110	109	sseli 3931	. . . . . . . . . . . . . 14 ⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℕ)
111		nnre 12166	. . . . . . . . . . . . . 14 ⊢ ((𝑌‘𝑗) ∈ ℕ → (𝑌‘𝑗) ∈ ℝ)
112	110, 111	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℝ)
113	108, 112	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ ℝ)
114	113	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ∈ ℝ)
115	30	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
116	115	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
117	116	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
118		simpl3 1195	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
119	70	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
120	119	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
121		breq1 5103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → (𝑥 < 𝑦 ↔ 𝑗 < 𝑦))
122		fveq2 6844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑋‘𝑥) = (𝑋‘𝑗))
123	122	breq1d 5110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝑦)))
124	121, 123	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦))))
125		breq2 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → (𝑗 < 𝑦 ↔ 𝑗 < 𝐼))
126		fveq2 6844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑋‘𝑦) = (𝑋‘𝐼))
127	126	breq2d 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑋‘𝑗) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
128	125, 127	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
129	124, 128	rspc2v 3589	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
130	118, 120, 129	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
131	117, 130	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))
132	131	syldbl2 842	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑋‘𝐼))
133		simp2 1138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
134		simp3 1139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼)
135	100	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ)
136	135	nnred 12174	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ)
137	103	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ)
138	136, 137	ltnled 11294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼 ≤ 𝑗))
139	134, 138	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼 ≤ 𝑗)
140	63	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
141	9	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
142		infrefilb 12142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)
143	142	3expia 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗))
144	140, 141, 143	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗))
145	144	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)
146	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ))
147	146	breq1d 5110	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → (𝐼 ≤ 𝑗 ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗))
148	145, 147	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 ≤ 𝑗)
149	148	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → 𝐼 ≤ 𝑗))
150	149	con3d 152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝐼 ≤ 𝑗 → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}))
151	139, 150	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
152		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧𝑗
153		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(1...𝐾)
154		nfv 1916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(𝑋‘𝑗) ≠ (𝑌‘𝑗)
155		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑋‘𝑧) = (𝑋‘𝑗))
156		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑌‘𝑧) = (𝑌‘𝑗))
157	155, 156	neeq12d 2994	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = 𝑗 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
158	152, 153, 154, 157	elrabf 3645	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
159	158	notbii 320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
160		ianor 984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
161	159, 160	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
162	151, 161	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
163		imor 854	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
164	162, 163	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
165	164	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))
166		nne 2937	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗) ↔ (𝑋‘𝑗) = (𝑌‘𝑗))
167	165, 166	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) = (𝑌‘𝑗))
168	133, 167	mpdan 688	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
169	168	3expa 1119	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
170	169	3adantl2 1169	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
171	170	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) = (𝑋‘𝑗))
172	171	breq1d 5110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌‘𝑗) < (𝑋‘𝐼) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
173	132, 172	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑋‘𝐼))
174	114, 173	ltned 11283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
175	76	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
176	175	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
177	176	necomd 2988	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
178		fveq2 6844	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑌‘𝑗) = (𝑌‘𝐼))
179	178	neeq1d 2992	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
180	179	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
181	177, 180	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
182	87	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
183	182	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
184	89	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
185	184	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
186	113	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ∈ ℝ)
187		simpl2 1194	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝐼))
188	42	simprd 495	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
189	188	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
190	189	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
191	119	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
192	107	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
193		breq1 5103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → (𝑥 < 𝑦 ↔ 𝐼 < 𝑦))
194		fveq2 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑌‘𝑥) = (𝑌‘𝐼))
195	194	breq1d 5110	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑦)))
196	193, 195	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦))))
197		breq2 5104	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → (𝐼 < 𝑦 ↔ 𝐼 < 𝑗))
198		fveq2 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑌‘𝑦) = (𝑌‘𝑗))
199	198	breq2d 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑌‘𝐼) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑗)))
200	197, 199	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
201	196, 200	rspc2v 3589	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
202	191, 192, 201	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
203	190, 202	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))
204	203	syldbl2 842	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑌‘𝑗))
205	183, 185, 186, 187, 204	lttrd 11308	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝑗))
206	183, 205	ltned 11283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ≠ (𝑌‘𝑗))
207	206	necomd 2988	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
208	174, 181, 207	3jaodan 1434	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
209	105, 208	mpdan 688	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
210	209	3expa 1119	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
211	210	neneqd 2938	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
212	211	ralrimiva 3130	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
213		ralnex 3064	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))
214	213	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
215		nnel 3047	. . . . . . . . . 10 ⊢ (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌)
216	215	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌))
217		fvelrnb 6904	. . . . . . . . . 10 ⊢ (𝑌 Fn (1...𝐾) → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
218	46, 217	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
219	216, 218	bitrd 279	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
220	219	con1bid 355	. . . . . . 7 ⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
221	214, 220	bitrd 279	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
222	221	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
223	212, 222	mpbid 232	. . . 4 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∉ ran 𝑌)
224		elnelne1 3048	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ran 𝑋 ∧ (𝑋‘𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌)
225	99, 223, 224	syl2anc 585	. . 3 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
226	45	ffund 6676	. . . . . 6 ⊢ (𝜑 → Fun 𝑌)
227	226	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → Fun 𝑌)
228	45	fdmd 6682	. . . . . . 7 ⊢ (𝜑 → dom 𝑌 = (1...𝐾))
229	70, 228	eleqtrrd 2840	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑌)
230	229	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → 𝐼 ∈ dom 𝑌)
231		fvelrn 7032	. . . . 5 ⊢ ((Fun 𝑌 ∧ 𝐼 ∈ dom 𝑌) → (𝑌‘𝐼) ∈ ran 𝑌)
232	227, 230, 231	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∈ ran 𝑌)
233	100	3ad2ant3 1136	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
234	233	nnred 12174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
235	103	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
236	234, 235	lttri4d 11288	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
237	31	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁))
238		simp3 1139	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
239	237, 238	ffvelcdmd 7041	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ (1...𝑁))
240	109	sseli 3931	. . . . . . . . . . . . . 14 ⊢ ((𝑋‘𝑗) ∈ (1...𝑁) → (𝑋‘𝑗) ∈ ℕ)
241	239, 240	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℕ)
242	241	nnred 12174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℝ)
243	242	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ∈ ℝ)
244	188	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
245	244	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
246		simpl3 1195	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
247	70	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
248	247	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
249		fveq2 6844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑌‘𝑥) = (𝑌‘𝑗))
250	249	breq1d 5110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝑦)))
251	121, 250	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦))))
252		fveq2 6844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑌‘𝑦) = (𝑌‘𝐼))
253	252	breq2d 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑌‘𝑗) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
254	125, 253	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
255	251, 254	rspc2v 3589	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
256	246, 248, 255	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
257	245, 256	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))
258	257	syldbl2 842	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑌‘𝐼))
259	169	3adantl2 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
260	259	breq1d 5110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋‘𝑗) < (𝑌‘𝐼) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
261	258, 260	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑌‘𝐼))
262	243, 261	ltned 11283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
263	89	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
264	263	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ∈ ℝ)
265		simpl2 1194	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) < (𝑋‘𝐼))
266	264, 265	ltned 11283	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
267	266	necomd 2988	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
268		fveq2 6844	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑋‘𝑗) = (𝑋‘𝐼))
269	268	neeq1d 2992	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
270	269	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
271	267, 270	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
272	263	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
273	87	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
274	273	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
275	242	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ∈ ℝ)
276		simpl2 1194	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝐼))
277	115	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
278	277	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
279	247	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
280	238	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
281		fveq2 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑋‘𝑥) = (𝑋‘𝐼))
282	281	breq1d 5110	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑦)))
283	193, 282	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦))))
284		fveq2 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑋‘𝑦) = (𝑋‘𝑗))
285	284	breq2d 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑋‘𝐼) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑗)))
286	197, 285	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
287	283, 286	rspc2v 3589	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
288	279, 280, 287	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
289	278, 288	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))
290	289	syldbl2 842	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑋‘𝑗))
291	272, 274, 275, 276, 290	lttrd 11308	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝑗))
292	272, 291	ltned 11283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ≠ (𝑋‘𝑗))
293	292	necomd 2988	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
294	262, 271, 293	3jaodan 1434	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
295	236, 294	mpdan 688	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
296	295	3expa 1119	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
297	296	neneqd 2938	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
298	297	ralrimiva 3130	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
299		ralnex 3064	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))
300	299	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
301		nnel 3047	. . . . . . . . . 10 ⊢ (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋)
302	301	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋))
303		fvelrnb 6904	. . . . . . . . . 10 ⊢ (𝑋 Fn (1...𝐾) → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
304	32, 303	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
305	302, 304	bitrd 279	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
306	305	con1bid 355	. . . . . . 7 ⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
307	300, 306	bitrd 279	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
308	307	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
309	298, 308	mpbid 232	. . . 4 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∉ ran 𝑋)
310		elnelne1 3048	. . . . 5 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋)
311	310	necomd 2988	. . . 4 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌)
312	232, 309, 311	syl2anc 585	. . 3 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
313	225, 312	jaodan 960	. 2 ⊢ ((𝜑 ∧ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) → ran 𝑋 ≠ ran 𝑌)
314	92, 313	mpdan 688	1 ⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∨ w3o 1086 ∧ w3a 1087 ∀wal 1540 = wceq 1542 ∈ wcel 2114 {cab 2715 ≠ wne 2933 ∉ wnel 3037 ∀wral 3052 ∃wrex 3062 {crab 3401 ⊆ wss 3903 ∅c0 4287 class class class wbr 5100 Or wor 5541 dom cdm 5634 ran crn 5635 Fun wfun 6496 Fn wfn 6497 ⟶wf 6498 ‘cfv 6502 (class class class)co 7370 Fincfn 8897 infcinf 9358 ℝcr 11039 1c1 11041 < clt 11180 ≤ cle 11181 ℕcn 12159 ℕ₀cn0 12415 ...cfz 13437

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-1st 7945 df-2nd 7946 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-er 8647 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-sup 9359 df-inf 9360 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-nn 12160 df-n0 12416 df-z 12503 df-uz 12766 df-fz 13438

This theorem is referenced by: sticksstones2 42546

W3C validator