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