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