Metamath Proof Explorer

Theorem sticksstones1

Description: Different strictly monotone functions have different ranges. (Contributed by metakunt, 27-Sep-2024)

Ref Expression
Hypotheses sticksstones1.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones1.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
sticksstones1.3 ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
sticksstones1.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
sticksstones1.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
sticksstones1.6 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
sticksstones1.7 ⊢ 𝐼 = inf ( { 𝑧 ∈ ( 1 ... 𝐾 ) ∣ ( 𝑋 ‘ 𝑧 ) ≠ ( 𝑌 ‘ 𝑧 ) } , ℝ , < )
Assertion sticksstones1 ( 𝜑 → ran 𝑋 ≠ ran 𝑌 )

Proof

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