This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ) ) ) )