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 42646

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 11221	. . . . . . 7 ⊢ < Or ℝ
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
5		fzfid 13930	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
6		ssrab2 4014	. . . . . . . . 9 ⊢ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾))
8		ssfi 9101	. . . . . . . 8 ⊢ (((1...𝐾) ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
9	5, 7, 8	syl2anc 591	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
10		sticksstones1.6	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11		rabeq0 4319	. . . . . . . . . . . . 13 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧))
12		nne 2940	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑧) = (𝑌‘𝑧))
13	12	ralbii 3087	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
14	11, 13	bitri 277	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
15		feq1 6637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁)))
16		fveq1 6830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑥) = (𝑋‘𝑥))
17		fveq1 6830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑦) = (𝑋‘𝑦))
18	16, 17	breq12d 5088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑋 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑋‘𝑥) < (𝑋‘𝑦)))
19	18	imbi2d 342	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
20	19	2ralbidv 3205	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑋 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
21	15, 20	anbi12d 639	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑋 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))))
22		sticksstones1.3	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}
23		eqabb 2880	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))))
24	22, 23	mpbi 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀𝑓(𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
25	24	spi 2198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ 𝐴 ↔ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
26	25	bilani 506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
27	26	ralrimiva 3133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
28		sticksstones1.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
29	21, 27, 28	rspcdva 3563	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
30	29	simpld 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋:(1...𝐾)⟶(1...𝑁))
31	30	ffnd 6660	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 Fn (1...𝐾))
32	31	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 Fn (1...𝐾))
33		sticksstones1.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 ∈ 𝐴)
34		feq1 6637	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑌:(1...𝐾)⟶(1...𝑁)))
35		fveq1 6830	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑥) = (𝑌‘𝑥))
36		fveq1 6830	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑦) = (𝑌‘𝑦))
37	35, 36	breq12d 5088	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑌 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑌‘𝑥) < (𝑌‘𝑦)))
38	37	imbi2d 342	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
39	38	2ralbidv 3205	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
40	34, 39	anbi12d 639	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))))
41	40, 27, 33	rspcdva 3563	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
42	41	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
43	33, 42	mpdan 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
44	43	simpld 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌:(1...𝐾)⟶(1...𝑁))
45	44	ffnd 6660	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 Fn (1...𝐾))
46	45	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑌 Fn (1...𝐾))
47		eqfnfv 6975	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 Fn (1...𝐾) ∧ 𝑌 Fn (1...𝐾)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)))
48	32, 46, 47	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (𝑋 = 𝑌 ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)))
49	48	bicomd 225	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) ↔ 𝑋 = 𝑌))
50	49	biimpd 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → (∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧) → 𝑋 = 𝑌))
51	50	syldbl2 848	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 = 𝑌)
52	14, 51	sylan2b 601	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅) → 𝑋 = 𝑌)
53	52	ex 414	. . . . . . . . . 10 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ → 𝑋 = 𝑌))
54	53	necon3d 2957	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ≠ 𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅))
55	54	imp 408	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
56	10, 55	mpdan 694	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
57		fz1ssnn 13504	. . . . . . . . . 10 ⊢ (1...𝐾) ⊆ ℕ
58	57	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1...𝐾) ⊆ ℕ)
59		nnssre 12173	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
60	59	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℕ ⊆ ℝ)
61	58, 60	sstrd 3927	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ⊆ ℝ)
62	7, 61	sstrd 3927	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
63	9, 56, 62	3jca 1135	. . . . . 6 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ))
64		fiinfcl 9410	. . . . . 6 ⊢ (( < Or ℝ ∧ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
65	4, 63, 64	syl2anc 591	. . . . 5 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
66	2, 65	eqeltrd 2841	. . . 4 ⊢ (𝜑 → 𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
67	7, 65	sseldd 3918	. . . . . 6 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾))
68	2	eleq1d 2826	. . . . . 6 ⊢ (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾)))
69	67, 68	mpbird 259	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (1...𝐾))
70		fveq2 6831	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑋‘𝑧) = (𝑋‘𝐼))
71		fveq2 6831	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑌‘𝑧) = (𝑌‘𝐼))
72	70, 71	neeq12d 2997	. . . . . 6 ⊢ (𝑧 = 𝐼 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
73	72	elrab3 3632	. . . . 5 ⊢ (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
74	69, 73	syl 17	. . . 4 ⊢ (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
75	66, 74	mpbid 234	. . 3 ⊢ (𝜑 → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
76		nfv 1922	. . . . . 6 ⊢ Ⅎ𝑎𝜑
77		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑎(1...𝑁)
78		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑎ℝ
79		elfznn 13502	. . . . . . . . 9 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
80	79	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ)
81		nnre 12176	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℝ)
82	80, 81	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ)
83	82	ex 414	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ))
84	76, 77, 78, 83	ssrd 3922	. . . . 5 ⊢ (𝜑 → (1...𝑁) ⊆ ℝ)
85	30, 69	ffvelcdmd 7030	. . . . 5 ⊢ (𝜑 → (𝑋‘𝐼) ∈ (1...𝑁))
86	84, 85	sseldd 3918	. . . 4 ⊢ (𝜑 → (𝑋‘𝐼) ∈ ℝ)
87	44, 69	ffvelcdmd 7030	. . . . 5 ⊢ (𝜑 → (𝑌‘𝐼) ∈ (1...𝑁))
88	84, 87	sseldd 3918	. . . 4 ⊢ (𝜑 → (𝑌‘𝐼) ∈ ℝ)
89		lttri2 11223	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ℝ ∧ (𝑌‘𝐼) ∈ ℝ) → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
90	86, 88, 89	syl2anc 591	. . 3 ⊢ (𝜑 → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
91	75, 90	mpbid 234	. 2 ⊢ (𝜑 → ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))
92	30	ffund 6663	. . . . . 6 ⊢ (𝜑 → Fun 𝑋)
93	92	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → Fun 𝑋)
94	30	fdmd 6669	. . . . . . 7 ⊢ (𝜑 → dom 𝑋 = (1...𝐾))
95	69, 94	eleqtrrd 2844	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑋)
96	95	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → 𝐼 ∈ dom 𝑋)
97		fvelrn 7021	. . . . 5 ⊢ ((Fun 𝑋 ∧ 𝐼 ∈ dom 𝑋) → (𝑋‘𝐼) ∈ ran 𝑋)
98	93, 96, 97	syl2anc 591	. . . 4 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∈ ran 𝑋)
99		elfznn 13502	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ)
100	99	3ad2ant3 1142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
101	100	nnred 12184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
102	61, 69	sseldd 3918	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
103	102	3ad2ant1 1140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
104	101, 103	lttri4d 11282	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
105	44	3ad2ant1 1140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁))
106		simp3 1145	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
107	105, 106	ffvelcdmd 7030	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ (1...𝑁))
108		fz1ssnn 13504	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
109	108	sseli 3913	. . . . . . . . . . . . . 14 ⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℕ)
110		nnre 12176	. . . . . . . . . . . . . 14 ⊢ ((𝑌‘𝑗) ∈ ℕ → (𝑌‘𝑗) ∈ ℝ)
111	109, 110	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℝ)
112	107, 111	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ ℝ)
113	112	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ∈ ℝ)
114	29	simprd 497	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
115	114	3ad2ant1 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
116	115	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
117		simpl3 1201	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
118	69	3ad2ant1 1140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
119	118	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
120		breq1 5078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → (𝑥 < 𝑦 ↔ 𝑗 < 𝑦))
121		fveq2 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑋‘𝑥) = (𝑋‘𝑗))
122	121	breq1d 5085	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝑦)))
123	120, 122	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦))))
124		breq2 5079	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → (𝑗 < 𝑦 ↔ 𝑗 < 𝐼))
125		fveq2 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑋‘𝑦) = (𝑋‘𝐼))
126	125	breq2d 5087	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑋‘𝑗) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
127	124, 126	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
128	123, 127	rspc2v 3573	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
129	117, 119, 128	syl2anc 591	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
130	116, 129	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼)))
131	130	syldbl2 848	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑋‘𝐼))
132		simp2 1144	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
133		simp3 1145	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼)
134	99	3ad2ant2 1141	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ)
135	134	nnred 12184	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ)
136	102	3ad2ant1 1140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ)
137	135, 136	ltnled 11288	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼 ≤ 𝑗))
138	133, 137	mpbid 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼 ≤ 𝑗)
139	62	3ad2ant1 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
140	9	3ad2ant1 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
141		infrefilb 12137	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)
142	141	3expia 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗))
143	139, 140, 142	syl2anc 591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗))
144	143	imp 408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)
145	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 = inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ))
146	145	breq1d 5085	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → (𝐼 ≤ 𝑗 ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗))
147	144, 146	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → 𝐼 ≤ 𝑗)
148	147	ex 414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} → 𝐼 ≤ 𝑗))
149	148	con3d 152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝐼 ≤ 𝑗 → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}))
150	138, 149	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
151		nfcv 2903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧𝑗
152		nfcv 2903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(1...𝐾)
153		nfv 1922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(𝑋‘𝑗) ≠ (𝑌‘𝑗)
154		fveq2 6831	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑋‘𝑧) = (𝑋‘𝑗))
155		fveq2 6831	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑌‘𝑧) = (𝑌‘𝑗))
156	154, 155	neeq12d 2997	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = 𝑗 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
157	151, 152, 153, 156	elrabf 3628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
158	157	notbii 322	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
159		ianor 990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
160	158, 159	bitri 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
161	150, 160	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
162		imor 860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
163	161, 162	sylibr 236	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
164	163	imp 408	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))
165		nne 2940	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗) ↔ (𝑋‘𝑗) = (𝑌‘𝑗))
166	164, 165	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) = (𝑌‘𝑗))
167	132, 166	mpdan 694	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
168	167	3expa 1125	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
169	168	3adantl2 1175	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
170	169	eqcomd 2747	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) = (𝑋‘𝑗))
171	170	breq1d 5085	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌‘𝑗) < (𝑋‘𝐼) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
172	131, 171	mpbird 259	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑋‘𝐼))
173	113, 172	ltned 11277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
174	75	3ad2ant1 1140	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
175	174	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
176	175	necomd 2991	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
177		fveq2 6831	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑌‘𝑗) = (𝑌‘𝐼))
178	177	neeq1d 2995	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
179	178	adantl 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
180	176, 179	mpbird 259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
181	86	3ad2ant1 1140	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
182	181	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
183	88	3ad2ant1 1140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
184	183	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
185	112	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ∈ ℝ)
186		simpl2 1200	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝐼))
187	41	simprd 497	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
188	187	3ad2ant1 1140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
189	188	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
190	118	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
191	106	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
192		breq1 5078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → (𝑥 < 𝑦 ↔ 𝐼 < 𝑦))
193		fveq2 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑌‘𝑥) = (𝑌‘𝐼))
194	193	breq1d 5085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑦)))
195	192, 194	imbi12d 346	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦))))
196		breq2 5079	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → (𝐼 < 𝑦 ↔ 𝐼 < 𝑗))
197		fveq2 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑌‘𝑦) = (𝑌‘𝑗))
198	197	breq2d 5087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑌‘𝐼) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑗)))
199	196, 198	imbi12d 346	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
200	195, 199	rspc2v 3573	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
201	190, 191, 200	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
202	189, 201	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗)))
203	202	syldbl2 848	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑌‘𝑗))
204	182, 184, 185, 186, 203	lttrd 11302	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝑗))
205	182, 204	ltned 11277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ≠ (𝑌‘𝑗))
206	205	necomd 2991	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
207	173, 180, 206	3jaodan 1440	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
208	104, 207	mpdan 694	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
209	208	3expa 1125	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
210	209	neneqd 2941	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
211	210	ralrimiva 3133	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
212		ralnex 3067	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))
213	212	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
214		nnel 3050	. . . . . . . . . 10 ⊢ (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌)
215	214	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌))
216		fvelrnb 6891	. . . . . . . . . 10 ⊢ (𝑌 Fn (1...𝐾) → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
217	45, 216	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
218	215, 217	bitrd 281	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
219	218	con1bid 357	. . . . . . 7 ⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
220	213, 219	bitrd 281	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
221	220	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ (𝑋‘𝐼) ∉ ran 𝑌))
222	211, 221	mpbid 234	. . . 4 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∉ ran 𝑌)
223		elnelne1 3051	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ran 𝑋 ∧ (𝑋‘𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌)
224	98, 222, 223	syl2anc 591	. . 3 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
225	44	ffund 6663	. . . . . 6 ⊢ (𝜑 → Fun 𝑌)
226	225	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → Fun 𝑌)
227	44	fdmd 6669	. . . . . . 7 ⊢ (𝜑 → dom 𝑌 = (1...𝐾))
228	69, 227	eleqtrrd 2844	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑌)
229	228	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → 𝐼 ∈ dom 𝑌)
230		fvelrn 7021	. . . . 5 ⊢ ((Fun 𝑌 ∧ 𝐼 ∈ dom 𝑌) → (𝑌‘𝐼) ∈ ran 𝑌)
231	226, 229, 230	syl2anc 591	. . . 4 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∈ ran 𝑌)
232	99	3ad2ant3 1142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
233	232	nnred 12184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
234	102	3ad2ant1 1140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
235	233, 234	lttri4d 11282	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
236	30	3ad2ant1 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁))
237		simp3 1145	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
238	236, 237	ffvelcdmd 7030	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ (1...𝑁))
239	108	sseli 3913	. . . . . . . . . . . . . 14 ⊢ ((𝑋‘𝑗) ∈ (1...𝑁) → (𝑋‘𝑗) ∈ ℕ)
240	238, 239	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℕ)
241	240	nnred 12184	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℝ)
242	241	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ∈ ℝ)
243	187	3ad2ant1 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
244	243	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
245		simpl3 1201	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
246	69	3ad2ant1 1140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
247	246	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
248		fveq2 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑌‘𝑥) = (𝑌‘𝑗))
249	248	breq1d 5085	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝑦)))
250	120, 249	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦))))
251		fveq2 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑌‘𝑦) = (𝑌‘𝐼))
252	251	breq2d 5087	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑌‘𝑗) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
253	124, 252	imbi12d 346	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
254	250, 253	rspc2v 3573	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (1...𝐾) ∧ 𝐼 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
255	245, 247, 254	syl2anc 591	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
256	244, 255	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼)))
257	256	syldbl2 848	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑌‘𝐼))
258	168	3adantl2 1175	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
259	258	breq1d 5085	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋‘𝑗) < (𝑌‘𝐼) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
260	257, 259	mpbird 259	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑌‘𝐼))
261	242, 260	ltned 11277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
262	88	3ad2ant1 1140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
263	262	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ∈ ℝ)
264		simpl2 1200	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) < (𝑋‘𝐼))
265	263, 264	ltned 11277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
266	265	necomd 2991	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
267		fveq2 6831	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑋‘𝑗) = (𝑋‘𝐼))
268	267	neeq1d 2995	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
269	268	adantl 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
270	266, 269	mpbird 259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
271	262	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
272	86	3ad2ant1 1140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
273	272	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
274	241	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ∈ ℝ)
275		simpl2 1200	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝐼))
276	114	3ad2ant1 1140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
277	276	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
278	246	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝐼 ∈ (1...𝐾))
279	237	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → 𝑗 ∈ (1...𝐾))
280		fveq2 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑋‘𝑥) = (𝑋‘𝐼))
281	280	breq1d 5085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑦)))
282	192, 281	imbi12d 346	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦))))
283		fveq2 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑋‘𝑦) = (𝑋‘𝑗))
284	283	breq2d 5087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑋‘𝐼) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑗)))
285	196, 284	imbi12d 346	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
286	282, 285	rspc2v 3573	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (1...𝐾) ∧ 𝑗 ∈ (1...𝐾)) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
287	278, 279, 286	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
288	277, 287	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗)))
289	288	syldbl2 848	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑋‘𝑗))
290	271, 273, 274, 275, 289	lttrd 11302	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝑗))
291	271, 290	ltned 11277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ≠ (𝑋‘𝑗))
292	291	necomd 2991	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
293	261, 270, 292	3jaodan 1440	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
294	235, 293	mpdan 694	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
295	294	3expa 1125	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
296	295	neneqd 2941	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
297	296	ralrimiva 3133	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
298		ralnex 3067	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))
299	298	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
300		nnel 3050	. . . . . . . . . 10 ⊢ (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋)
301	300	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋))
302		fvelrnb 6891	. . . . . . . . . 10 ⊢ (𝑋 Fn (1...𝐾) → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
303	31, 302	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
304	301, 303	bitrd 281	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
305	304	con1bid 357	. . . . . . 7 ⊢ (𝜑 → (¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
306	299, 305	bitrd 281	. . . . . 6 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
307	306	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ (𝑌‘𝐼) ∉ ran 𝑋))
308	297, 307	mpbid 234	. . . 4 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∉ ran 𝑋)
309		elnelne1 3051	. . . . 5 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋)
310	309	necomd 2991	. . . 4 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌)
311	231, 308, 310	syl2anc 591	. . 3 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
312	224, 311	jaodan 966	. 2 ⊢ ((𝜑 ∧ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) → ran 𝑋 ≠ ran 𝑌)
313	91, 312	mpdan 694	1 ⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 ∨ wo 854 ∨ w3o 1092 ∧ w3a 1093 ∀wal 1546 = wceq 1548 ∈ wcel 2121 {cab 2719 ≠ wne 2936 ∉ wnel 3040 ∀wral 3055 ∃wrex 3065 {crab 3393 ⊆ wss 3885 ∅c0 4264 class class class wbr 5075 Or wor 5528 dom cdm 5621 ran crn 5622 Fun wfun 6483 Fn wfn 6484 ⟶wf 6485 ‘cfv 6489 (class class class)co 7360 Fincfn 8887 infcinf 9348 ℝcr 11032 1c1 11034 < clt 11174 ≤ cle 11175 ℕcn 12169 ℕ₀cn0 12432 ...cfz 13456

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 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-inf 9350 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-n0 12433 df-z 12520 df-uz 12784 df-fz 13457

This theorem is referenced by: sticksstones2 42647

W3C validator