icceuelpart

Description: An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020)

	Ref	Expression
Hypotheses	iccpartiun.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	iccpartiun.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion	icceuelpart	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → ∃! 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccpartiun.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		iccpartiun.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
4		iccelpart	⊢ ( 𝑀 ∈ ℕ → ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
5	1 4	syl	⊢ ( 𝜑 → ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
7		fveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
8		fveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑀 ) )
9	7 8	oveq12d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) = ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) )
10	9	eleq2d	⊢ ( 𝑝 = 𝑃 → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) ↔ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) )
11		fveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
12		fveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
13	11 12	oveq12d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
14	13	eleq2d	⊢ ( 𝑝 = 𝑃 → ( 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
15	14	rexbidv	⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
16	10 15	imbi12d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) ) )
17	16	rspcva	⊢ ( ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
18	17	adantld	⊢ ( ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
19	18	com12	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → ( ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
20	3 6 19	mp2and	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
21	1	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ )
22	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
23		elfzofz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
25	21 22 24	iccpartxr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ^* )
26		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
28	21 22 27	iccpartxr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ^* )
29	25 28	jca	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ^* ) )
30	29	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ^* ) )
31		elico1	⊢ ( ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ^* ) → ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
32	30 31	syl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
33	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ )
34	2	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
35		elfzofz	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
36	35	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
37	33 34 36	iccpartxr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ^* )
38		fzofzp1	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
39	38	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
40	33 34 39	iccpartxr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ^* )
41	37 40	jca	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑗 ) ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ^* ) )
42	41	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ 𝑗 ) ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ^* ) )
43		elico1	⊢ ( ( ( 𝑃 ‘ 𝑗 ) ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ^* ) → ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) )
44	42 43	syl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) )
45	32 44	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) ↔ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) ) )
46		elfzoelz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ℤ )
47	46	zred	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ℝ )
48		elfzoelz	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℤ )
49	48	zred	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℝ )
50	47 49	anim12i	⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) )
51	50	adantl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) )
52		lttri4	⊢ ( ( 𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖 ) )
53	51 52	syl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖 ) )
54	1 2	icceuelpartlem	⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) ) )
55	54	imp31	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) )
56		simpl	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → 𝑋 ∈ ℝ^* )
57	28	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ^* )
58	57	adantl	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ^* )
59	37	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ^* )
60	59	adantl	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ^* )
61		nltle2tri	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ∈ ℝ^* ) → ¬ ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ) )
62	56 58 60 61	syl3anc	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ¬ ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ) )
63	62	pm2.21d	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ) → 𝑖 = 𝑗 ) )
64	63	3expd	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) → ( ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 → 𝑖 = 𝑗 ) ) ) )
65	64	ex	⊢ ( 𝑋 ∈ ℝ^* → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) → ( ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 → 𝑖 = 𝑗 ) ) ) ) )
66	65	com23	⊢ ( 𝑋 ∈ ℝ^* → ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) → ( ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 → 𝑖 = 𝑗 ) ) ) ) )
67	66	com25	⊢ ( 𝑋 ∈ ℝ^* → ( ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → 𝑖 = 𝑗 ) ) ) ) )
68	67	imp4b	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → 𝑖 = 𝑗 ) ) )
69	68	com23	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) → 𝑖 = 𝑗 ) ) )
70	69	3adant3	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) → 𝑖 = 𝑗 ) ) )
71	70	com12	⊢ ( 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) → 𝑖 = 𝑗 ) ) )
72	71	3ad2ant3	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) → 𝑖 = 𝑗 ) ) )
73	72	imp	⊢ ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) → 𝑖 = 𝑗 ) )
74	73	com12	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑗 ) ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
75	55 74	syldan	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝑖 < 𝑗 ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
76	75	expcom	⊢ ( 𝑖 < 𝑗 → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) ) )
77		2a1	⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) ) )
78	1 2	icceuelpartlem	⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑗 < 𝑖 → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) ) )
79	78	ancomsd	⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑗 < 𝑖 → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) ) )
80	79	imp31	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝑗 < 𝑖 ) → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) )
81	40	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ^* )
82	81	adantl	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ^* )
83	25	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ^* )
84	83	adantl	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ^* )
85		nltle2tri	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ∈ ℝ^* ) → ¬ ( 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ) )
86	56 82 84 85	syl3anc	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ¬ ( 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ) )
87	86	pm2.21d	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( ( 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ) → 𝑖 = 𝑗 ) )
88	87	3expd	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) → ( ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) → ( ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 → 𝑖 = 𝑗 ) ) ) )
89	88	ex	⊢ ( 𝑋 ∈ ℝ^* → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) → ( ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) → ( ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 → 𝑖 = 𝑗 ) ) ) ) )
90	89	com23	⊢ ( 𝑋 ∈ ℝ^* → ( 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) → ( ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 → 𝑖 = 𝑗 ) ) ) ) )
91	90	imp4b	⊢ ( ( 𝑋 ∈ ℝ^* ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) → ( ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 → 𝑖 = 𝑗 ) ) )
92	91	com23	⊢ ( ( 𝑋 ∈ ℝ^* ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) → 𝑖 = 𝑗 ) ) )
93	92	3adant2	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) → 𝑖 = 𝑗 ) ) )
94	93	com12	⊢ ( ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 → ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) → 𝑖 = 𝑗 ) ) )
95	94	3ad2ant2	⊢ ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) → 𝑖 = 𝑗 ) ) )
96	95	imp	⊢ ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) → 𝑖 = 𝑗 ) )
97	96	com12	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ ( 𝑃 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑃 ‘ 𝑖 ) ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
98	80 97	syldan	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) ∧ 𝑗 < 𝑖 ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
99	98	expcom	⊢ ( 𝑗 < 𝑖 → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) ) )
100	76 77 99	3jaoi	⊢ ( ( 𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖 ) → ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) ) )
101	53 100	mpcom	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑖 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ^* ∧ ( 𝑃 ‘ 𝑗 ) ≤ 𝑋 ∧ 𝑋 < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
102	45 101	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
103	102	ralrimivva	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∀ 𝑗 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
104	103	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∀ 𝑗 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) )
105		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑗 ) )
106		fvoveq1	⊢ ( 𝑖 = 𝑗 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
107	105 106	oveq12d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) )
108	107	eleq2d	⊢ ( 𝑖 = 𝑗 → ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) )
109	108	reu4	⊢ ( ∃! 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∀ 𝑗 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑃 ‘ 𝑗 ) [,) ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 = 𝑗 ) ) )
110	20 104 109	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ( 𝑃 ‘ 0 ) [,) ( 𝑃 ‘ 𝑀 ) ) ) → ∃! 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑃 ‘ 𝑖 ) [,) ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )

Metamath Proof Explorer

Theorem icceuelpart

Proof