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 40102

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 11055	. . . . . . 7 ⊢ < Or ℝ
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
5		fzfid 13693	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
6		ssrab2 4013	. . . . . . . . 9 ⊢ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾))
8		ssfi 8956	. . . . . . . 8 ⊢ (((1...𝐾) ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ (1...𝐾)) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
9	5, 7, 8	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
10		sticksstones1.6	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11		rabeq0 4318	. . . . . . . . . . . . 13 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧))
12		nne 2947	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑧) = (𝑌‘𝑧))
13	12	ralbii 3092	. . . . . . . . . . . . 13 ⊢ (∀𝑧 ∈ (1...𝐾) ¬ (𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
14	11, 13	bitri 274	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ ↔ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧))
15		feq1 6581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑋 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑋:(1...𝐾)⟶(1...𝑁)))
16		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑥) = (𝑋‘𝑥))
17		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑋 → (𝑓‘𝑦) = (𝑋‘𝑦))
18	16, 17	breq12d 5087	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑋 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑋‘𝑥) < (𝑋‘𝑦)))
19	18	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑋 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
20	19	2ralbidv 3129	. . . . . . . . . . . . . . . . . . . . 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		abeq2 2872	. . . . . . . . . . . . . . . . . . . . . . . . 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 3103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))))
29		sticksstones1.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
30	21, 28, 29	rspcdva 3562	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑋:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦))))
31	30	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋:(1...𝐾)⟶(1...𝑁))
32	31	ffnd 6601	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 Fn (1...𝐾))
33	32	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 Fn (1...𝐾))
34		sticksstones1.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑌 ∈ 𝐴)
35		feq1 6581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑌:(1...𝐾)⟶(1...𝑁)))
36		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑥) = (𝑌‘𝑥))
37		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑌 → (𝑓‘𝑦) = (𝑌‘𝑦))
38	36, 37	breq12d 5087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑌 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑌‘𝑥) < (𝑌‘𝑦)))
39	38	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑌 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
40	39	2ralbidv 3129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑌 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
41	35, 40	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑌 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))))
42	41, 28, 34	rspcdva 3562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
43	42	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
44	34, 43	mpdan 684	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑌:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦))))
45	44	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌:(1...𝐾)⟶(1...𝑁))
46	45	ffnd 6601	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 Fn (1...𝐾))
47	46	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑌 Fn (1...𝐾))
48		eqfnfv 6909	. . . . . . . . . . . . . . . 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 838	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑧 ∈ (1...𝐾)(𝑋‘𝑧) = (𝑌‘𝑧)) → 𝑋 = 𝑌)
53	14, 52	sylan2b 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅) → 𝑋 = 𝑌)
54	53	ex 413	. . . . . . . . . 10 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} = ∅ → 𝑋 = 𝑌))
55	54	necon3d 2964	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ≠ 𝑌 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅))
56	55	imp 407	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
57	10, 56	mpdan 684	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅)
58		fz1ssnn 13287	. . . . . . . . . 10 ⊢ (1...𝐾) ⊆ ℕ
59	58	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1...𝐾) ⊆ ℕ)
60		nnssre 11977	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
61	60	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℕ ⊆ ℝ)
62	59, 61	sstrd 3931	. . . . . . . 8 ⊢ (𝜑 → (1...𝐾) ⊆ ℝ)
63	7, 62	sstrd 3931	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
64	9, 57, 63	3jca 1127	. . . . . 6 ⊢ (𝜑 → ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ))
65		fiinfcl 9260	. . . . . 6 ⊢ (( < Or ℝ ∧ ({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ≠ ∅ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
66	4, 64, 65	syl2anc 584	. . . . 5 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
67	2, 66	eqeltrd 2839	. . . 4 ⊢ (𝜑 → 𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)})
68	7, 66	sseldd 3922	. . . . . 6 ⊢ (𝜑 → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾))
69	2	eleq1d 2823	. . . . . 6 ⊢ (𝜑 → (𝐼 ∈ (1...𝐾) ↔ inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ∈ (1...𝐾)))
70	68, 69	mpbird 256	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (1...𝐾))
71		fveq2 6774	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑋‘𝑧) = (𝑋‘𝐼))
72		fveq2 6774	. . . . . . 7 ⊢ (𝑧 = 𝐼 → (𝑌‘𝑧) = (𝑌‘𝐼))
73	71, 72	neeq12d 3005	. . . . . 6 ⊢ (𝑧 = 𝐼 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
74	73	elrab3 3625	. . . . 5 ⊢ (𝐼 ∈ (1...𝐾) → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
75	70, 74	syl 17	. . . 4 ⊢ (𝜑 → (𝐼 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
76	67, 75	mpbid 231	. . 3 ⊢ (𝜑 → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
77		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑎𝜑
78		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑎(1...𝑁)
79		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑎ℝ
80		elfznn 13285	. . . . . . . . 9 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
81	80	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℕ)
82		nnre 11980	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℝ)
83	81, 82	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑁)) → 𝑎 ∈ ℝ)
84	83	ex 413	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℝ))
85	77, 78, 79, 84	ssrd 3926	. . . . 5 ⊢ (𝜑 → (1...𝑁) ⊆ ℝ)
86	31, 70	ffvelrnd 6962	. . . . 5 ⊢ (𝜑 → (𝑋‘𝐼) ∈ (1...𝑁))
87	85, 86	sseldd 3922	. . . 4 ⊢ (𝜑 → (𝑋‘𝐼) ∈ ℝ)
88	45, 70	ffvelrnd 6962	. . . . 5 ⊢ (𝜑 → (𝑌‘𝐼) ∈ (1...𝑁))
89	85, 88	sseldd 3922	. . . 4 ⊢ (𝜑 → (𝑌‘𝐼) ∈ ℝ)
90		lttri2 11057	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ℝ ∧ (𝑌‘𝐼) ∈ ℝ) → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
91	87, 89, 90	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝑋‘𝐼) ≠ (𝑌‘𝐼) ↔ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))))
92	76, 91	mpbid 231	. 2 ⊢ (𝜑 → ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼)))
93	31	ffund 6604	. . . . . 6 ⊢ (𝜑 → Fun 𝑋)
94	93	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → Fun 𝑋)
95	31	fdmd 6611	. . . . . . 7 ⊢ (𝜑 → dom 𝑋 = (1...𝐾))
96	70, 95	eleqtrrd 2842	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑋)
97	96	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → 𝐼 ∈ dom 𝑋)
98		fvelrn 6954	. . . . 5 ⊢ ((Fun 𝑋 ∧ 𝐼 ∈ dom 𝑋) → (𝑋‘𝐼) ∈ ran 𝑋)
99	94, 97, 98	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → (𝑋‘𝐼) ∈ ran 𝑋)
100		elfznn 13285	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝐾) → 𝑗 ∈ ℕ)
101	100	3ad2ant3 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
102	101	nnred 11988	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
103	62, 70	sseldd 3922	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℝ)
104	103	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
105	102, 104	lttri4d 11116	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
106	45	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑌:(1...𝐾)⟶(1...𝑁))
107		simp3 1137	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
108	106, 107	ffvelrnd 6962	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ∈ (1...𝑁))
109		fz1ssnn 13287	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
110	109	sseli 3917	. . . . . . . . . . . . . 14 ⊢ ((𝑌‘𝑗) ∈ (1...𝑁) → (𝑌‘𝑗) ∈ ℕ)
111		nnre 11980	. . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
117	116	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)))
118		simpl3 1192	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
119	70	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
120	119	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
121		breq1 5077	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → (𝑥 < 𝑦 ↔ 𝑗 < 𝑦))
122		fveq2 6774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑋‘𝑥) = (𝑋‘𝑗))
123	122	breq1d 5084	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝑦)))
124	121, 123	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦))))
125		breq2 5078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → (𝑗 < 𝑦 ↔ 𝑗 < 𝐼))
126		fveq2 6774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑋‘𝑦) = (𝑋‘𝐼))
127	126	breq2d 5086	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑋‘𝑗) < (𝑋‘𝑦) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
128	125, 127	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑋‘𝑗) < (𝑋‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑋‘𝑗) < (𝑋‘𝐼))))
129	124, 128	rspc2v 3570	. . . . . . . . . . . . . . 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 838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑋‘𝐼))
133		simp2 1136	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
134		simp3 1137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 < 𝐼)
135	100	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℕ)
136	135	nnred 11988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝑗 ∈ ℝ)
137	103	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → 𝐼 ∈ ℝ)
138	136, 137	ltnled 11122	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 < 𝐼 ↔ ¬ 𝐼 ≤ 𝑗))
139	134, 138	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → ¬ 𝐼 ≤ 𝑗)
140	63	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ)
141	9	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin)
142		infrefilb 11961	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ⊆ ℝ ∧ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ∈ Fin ∧ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}) → inf({𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)}, ℝ, < ) ≤ 𝑗)
143	142	3expia 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5084	. . . . . . . . . . . . . . . . . . . . . . . . 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 2907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧𝑗
153		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(1...𝐾)
154		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑧(𝑋‘𝑗) ≠ (𝑌‘𝑗)
155		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑋‘𝑧) = (𝑋‘𝑗))
156		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑗 → (𝑌‘𝑧) = (𝑌‘𝑗))
157	155, 156	neeq12d 3005	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = 𝑗 → ((𝑋‘𝑧) ≠ (𝑌‘𝑧) ↔ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
158	152, 153, 154, 157	elrabf 3620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
159	158	notbii 320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ ¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
160		ianor 979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ (𝑗 ∈ (1...𝐾) ∧ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
161	159, 160	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑗 ∈ {𝑧 ∈ (1...𝐾) ∣ (𝑋‘𝑧) ≠ (𝑌‘𝑧)} ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
162	151, 161	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
163		imor 850	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)) ↔ (¬ 𝑗 ∈ (1...𝐾) ∨ ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
164	162, 163	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑗 ∈ (1...𝐾) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗)))
165	164	imp 407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗))
166		nne 2947	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑋‘𝑗) ≠ (𝑌‘𝑗) ↔ (𝑋‘𝑗) = (𝑌‘𝑗))
167	165, 166	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) = (𝑌‘𝑗))
168	133, 167	mpdan 684	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝐾) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
169	168	3expa 1117	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
170	169	3adantl2 1166	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
171	170	eqcomd 2744	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) = (𝑋‘𝑗))
172	171	breq1d 5084	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑌‘𝑗) < (𝑋‘𝐼) ↔ (𝑋‘𝑗) < (𝑋‘𝐼)))
173	132, 172	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑋‘𝐼))
174	114, 173	ltned 11111	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
175	76	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
176	175	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
177	176	necomd 2999	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
178		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑌‘𝑗) = (𝑌‘𝐼))
179	178	neeq1d 3003	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
180	179	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑌‘𝑗) ≠ (𝑋‘𝐼) ↔ (𝑌‘𝐼) ≠ (𝑋‘𝐼)))
181	177, 180	mpbird 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
182	87	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
183	182	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
184	89	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
185	184	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
186	113	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ∈ ℝ)
187		simpl2 1191	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝐼))
188	42	simprd 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
189	188	3ad2ant1 1132	. . . . . . . . . . . . . . . 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 5077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → (𝑥 < 𝑦 ↔ 𝐼 < 𝑦))
194		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑌‘𝑥) = (𝑌‘𝐼))
195	194	breq1d 5084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑦)))
196	193, 195	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦))))
197		breq2 5078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → (𝐼 < 𝑦 ↔ 𝐼 < 𝑗))
198		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑌‘𝑦) = (𝑌‘𝑗))
199	198	breq2d 5086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑌‘𝐼) < (𝑌‘𝑦) ↔ (𝑌‘𝐼) < (𝑌‘𝑗)))
200	197, 199	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑌‘𝐼) < (𝑌‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑌‘𝐼) < (𝑌‘𝑗))))
201	196, 200	rspc2v 3570	. . . . . . . . . . . . . . . 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 838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑌‘𝑗))
205	183, 185, 186, 187, 204	lttrd 11136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑌‘𝑗))
206	183, 205	ltned 11111	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ≠ (𝑌‘𝑗))
207	206	necomd 2999	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
208	174, 181, 207	3jaodan 1429	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
209	105, 208	mpdan 684	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
210	209	3expa 1117	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝑗) ≠ (𝑋‘𝐼))
211	210	neneqd 2948	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
212	211	ralrimiva 3103	. . . . 5 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼))
213		ralnex 3167	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼))
214	213	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑌‘𝑗) = (𝑋‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
215		nnel 3058	. . . . . . . . . 10 ⊢ (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌)
216	215	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ (𝑋‘𝐼) ∈ ran 𝑌))
217		fvelrnb 6830	. . . . . . . . . 10 ⊢ (𝑌 Fn (1...𝐾) → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
218	46, 217	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋‘𝐼) ∈ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
219	216, 218	bitrd 278	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑋‘𝐼) ∉ ran 𝑌 ↔ ∃𝑗 ∈ (1...𝐾)(𝑌‘𝑗) = (𝑋‘𝐼)))
220	219	con1bid 356	. . . . . . 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 3059	. . . 4 ⊢ (((𝑋‘𝐼) ∈ ran 𝑋 ∧ (𝑋‘𝐼) ∉ ran 𝑌) → ran 𝑋 ≠ ran 𝑌)
225	99, 223, 224	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ (𝑋‘𝐼) < (𝑌‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
226	45	ffund 6604	. . . . . 6 ⊢ (𝜑 → Fun 𝑌)
227	226	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → Fun 𝑌)
228	45	fdmd 6611	. . . . . . 7 ⊢ (𝜑 → dom 𝑌 = (1...𝐾))
229	70, 228	eleqtrrd 2842	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ dom 𝑌)
230	229	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → 𝐼 ∈ dom 𝑌)
231		fvelrn 6954	. . . . 5 ⊢ ((Fun 𝑌 ∧ 𝐼 ∈ dom 𝑌) → (𝑌‘𝐼) ∈ ran 𝑌)
232	227, 230, 231	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → (𝑌‘𝐼) ∈ ran 𝑌)
233	100	3ad2ant3 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℕ)
234	233	nnred 11988	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ ℝ)
235	103	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ ℝ)
236	234, 235	lttri4d 11116	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗))
237	31	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑋:(1...𝐾)⟶(1...𝑁))
238		simp3 1137	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾))
239	237, 238	ffvelrnd 6962	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ (1...𝑁))
240	109	sseli 3917	. . . . . . . . . . . . . 14 ⊢ ((𝑋‘𝑗) ∈ (1...𝑁) → (𝑋‘𝑗) ∈ ℕ)
241	239, 240	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℕ)
242	241	nnred 11988	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ∈ ℝ)
243	242	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ∈ ℝ)
244	188	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
245	244	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)))
246		simpl3 1192	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝑗 ∈ (1...𝐾))
247	70	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → 𝐼 ∈ (1...𝐾))
248	247	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → 𝐼 ∈ (1...𝐾))
249		fveq2 6774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑗 → (𝑌‘𝑥) = (𝑌‘𝑗))
250	249	breq1d 5084	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑗 → ((𝑌‘𝑥) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝑦)))
251	121, 250	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑗 → ((𝑥 < 𝑦 → (𝑌‘𝑥) < (𝑌‘𝑦)) ↔ (𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦))))
252		fveq2 6774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝐼 → (𝑌‘𝑦) = (𝑌‘𝐼))
253	252	breq2d 5086	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐼 → ((𝑌‘𝑗) < (𝑌‘𝑦) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
254	125, 253	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐼 → ((𝑗 < 𝑦 → (𝑌‘𝑗) < (𝑌‘𝑦)) ↔ (𝑗 < 𝐼 → (𝑌‘𝑗) < (𝑌‘𝐼))))
255	251, 254	rspc2v 3570	. . . . . . . . . . . . . . 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 838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑌‘𝑗) < (𝑌‘𝐼))
259	169	3adantl2 1166	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) = (𝑌‘𝑗))
260	259	breq1d 5084	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → ((𝑋‘𝑗) < (𝑌‘𝐼) ↔ (𝑌‘𝑗) < (𝑌‘𝐼)))
261	258, 260	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) < (𝑌‘𝐼))
262	243, 261	ltned 11111	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 < 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
263	89	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑌‘𝐼) ∈ ℝ)
264	263	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ∈ ℝ)
265		simpl2 1191	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) < (𝑋‘𝐼))
266	264, 265	ltned 11111	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑌‘𝐼) ≠ (𝑋‘𝐼))
267	266	necomd 2999	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝐼) ≠ (𝑌‘𝐼))
268		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (𝑋‘𝑗) = (𝑋‘𝐼))
269	268	neeq1d 3003	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
270	269	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → ((𝑋‘𝑗) ≠ (𝑌‘𝐼) ↔ (𝑋‘𝐼) ≠ (𝑌‘𝐼)))
271	267, 270	mpbird 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑗 = 𝐼) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
272	263	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ∈ ℝ)
273	87	3ad2ant1 1132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝐼) ∈ ℝ)
274	273	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) ∈ ℝ)
275	242	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ∈ ℝ)
276		simpl2 1191	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝐼))
277	115	3ad2ant1 1132	. . . . . . . . . . . . . . . 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 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐼 → (𝑋‘𝑥) = (𝑋‘𝐼))
282	281	breq1d 5084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐼 → ((𝑋‘𝑥) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑦)))
283	193, 282	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝐼 → ((𝑥 < 𝑦 → (𝑋‘𝑥) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦))))
284		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑗 → (𝑋‘𝑦) = (𝑋‘𝑗))
285	284	breq2d 5086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑗 → ((𝑋‘𝐼) < (𝑋‘𝑦) ↔ (𝑋‘𝐼) < (𝑋‘𝑗)))
286	197, 285	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → ((𝐼 < 𝑦 → (𝑋‘𝐼) < (𝑋‘𝑦)) ↔ (𝐼 < 𝑗 → (𝑋‘𝐼) < (𝑋‘𝑗))))
287	283, 286	rspc2v 3570	. . . . . . . . . . . . . . . 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 838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝐼) < (𝑋‘𝑗))
291	272, 274, 275, 276, 290	lttrd 11136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) < (𝑋‘𝑗))
292	272, 291	ltned 11111	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑌‘𝐼) ≠ (𝑋‘𝑗))
293	292	necomd 2999	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝐼 < 𝑗) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
294	262, 271, 293	3jaodan 1429	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) ∧ (𝑗 < 𝐼 ∨ 𝑗 = 𝐼 ∨ 𝐼 < 𝑗)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
295	236, 294	mpdan 684	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
296	295	3expa 1117	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → (𝑋‘𝑗) ≠ (𝑌‘𝐼))
297	296	neneqd 2948	. . . . . 6 ⊢ (((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) ∧ 𝑗 ∈ (1...𝐾)) → ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
298	297	ralrimiva 3103	. . . . 5 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼))
299		ralnex 3167	. . . . . . . 8 ⊢ (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼))
300	299	a1i 11	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (1...𝐾) ¬ (𝑋‘𝑗) = (𝑌‘𝐼) ↔ ¬ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
301		nnel 3058	. . . . . . . . . 10 ⊢ (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋)
302	301	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ (𝑌‘𝐼) ∈ ran 𝑋))
303		fvelrnb 6830	. . . . . . . . . 10 ⊢ (𝑋 Fn (1...𝐾) → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
304	32, 303	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌‘𝐼) ∈ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
305	302, 304	bitrd 278	. . . . . . . 8 ⊢ (𝜑 → (¬ (𝑌‘𝐼) ∉ ran 𝑋 ↔ ∃𝑗 ∈ (1...𝐾)(𝑋‘𝑗) = (𝑌‘𝐼)))
306	305	con1bid 356	. . . . . . 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 3059	. . . . 5 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑌 ≠ ran 𝑋)
311	310	necomd 2999	. . . 4 ⊢ (((𝑌‘𝐼) ∈ ran 𝑌 ∧ (𝑌‘𝐼) ∉ ran 𝑋) → ran 𝑋 ≠ ran 𝑌)
312	232, 309, 311	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ (𝑌‘𝐼) < (𝑋‘𝐼)) → ran 𝑋 ≠ ran 𝑌)
313	225, 312	jaodan 955	. 2 ⊢ ((𝜑 ∧ ((𝑋‘𝐼) < (𝑌‘𝐼) ∨ (𝑌‘𝐼) < (𝑋‘𝐼))) → ran 𝑋 ≠ ran 𝑌)
314	92, 313	mpdan 684	1 ⊢ (𝜑 → ran 𝑋 ≠ ran 𝑌)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∨ w3o 1085 ∧ w3a 1086 ∀wal 1537 = wceq 1539 ∈ wcel 2106 {cab 2715 ≠ wne 2943 ∉ wnel 3049 ∀wral 3064 ∃wrex 3065 {crab 3068 ⊆ wss 3887 ∅c0 4256 class class class wbr 5074 Or wor 5502 dom cdm 5589 ran crn 5590 Fun wfun 6427 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 Fincfn 8733 infcinf 9200 ℝcr 10870 1c1 10872 < clt 11009 ≤ cle 11010 ℕcn 11973 ℕ₀cn0 12233 ...cfz 13239

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-n0 12234 df-z 12320 df-uz 12583 df-fz 13240

This theorem is referenced by: sticksstones2 40103

W3C validator