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