Metamath Proof Explorer

Theorem injresinjlem

Description: Lemma for injresinj . (Contributed by Alexander van der Vekens, 31-Oct-2017) (Proof shortened by AV, 14-Feb-2021) (Revised by Thierry Arnoux, 23-Dec-2021)

Ref Expression
Assertion injresinjlem ( ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑋 ∈ ( 0 ... 𝐾 ) ∧ 𝑌 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elfznelfzo ⊢ ( ( 𝑌 ∈ ( 0 ... 𝐾 ) ∧ ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) ) → ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) )
2 fvinim0ffz ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ↔ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) ) )
3 df-nel ⊢ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) )
4 fveq2 ⊢ ( 0 = 𝑌 → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 𝑌 ) )
5 4 eqcoms ⊢ ( 𝑌 = 0 → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 𝑌 ) )
6 5 eleq1d ⊢ ( 𝑌 = 0 → ( ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
7 6 notbid ⊢ ( 𝑌 = 0 → ( ¬ ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
8 7 biimpd ⊢ ( 𝑌 = 0 → ( ¬ ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ¬ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
9 ffn ⊢ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → 𝐹 Fn ( 0 ... 𝐾 ) )
10 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
11 fzoss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ..^ 𝐾 ) ⊆ ( 0 ..^ 𝐾 ) )
12 10 11 mp1i ⊢ ( 𝐾 ∈ ℕ0 → ( 1 ..^ 𝐾 ) ⊆ ( 0 ..^ 𝐾 ) )
13 fzossfz ⊢ ( 0 ..^ 𝐾 ) ⊆ ( 0 ... 𝐾 )
14 12 13 sstrdi ⊢ ( 𝐾 ∈ ℕ0 → ( 1 ..^ 𝐾 ) ⊆ ( 0 ... 𝐾 ) )
15 fvelimab ⊢ ( ( 𝐹 Fn ( 0 ... 𝐾 ) ∧ ( 1 ..^ 𝐾 ) ⊆ ( 0 ... 𝐾 ) ) → ( ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ∃ 𝑧 ∈ ( 1 ..^ 𝐾 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ) )
16 9 14 15 syl2an ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ∃ 𝑧 ∈ ( 1 ..^ 𝐾 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ) )
17 16 notbid ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ¬ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ∃ 𝑧 ∈ ( 1 ..^ 𝐾 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ) )
18 ralnex ⊢ ( ∀ 𝑧 ∈ ( 1 ..^ 𝐾 ) ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ↔ ¬ ∃ 𝑧 ∈ ( 1 ..^ 𝐾 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) )
19 fveqeq2 ⊢ ( 𝑧 = 𝑋 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )
20 19 notbid ⊢ ( 𝑧 = 𝑋 → ( ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ↔ ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )
21 20 rspcva ⊢ ( ( 𝑋 ∈ ( 1 ..^ 𝐾 ) ∧ ∀ 𝑧 ∈ ( 1 ..^ 𝐾 ) ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ) → ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
22 pm2.21 ⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
23 22 a1d ⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
24 23 2a1d ⊢ ( ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
25 21 24 syl ⊢ ( ( 𝑋 ∈ ( 1 ..^ 𝐾 ) ∧ ∀ 𝑧 ∈ ( 1 ..^ 𝐾 ) ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
26 25 expcom ⊢ ( ∀ 𝑧 ∈ ( 1 ..^ 𝐾 ) ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
27 26 com24 ⊢ ( ∀ 𝑧 ∈ ( 1 ..^ 𝐾 ) ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
28 18 27 sylbir ⊢ ( ¬ ∃ 𝑧 ∈ ( 1 ..^ 𝐾 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
29 28 com12 ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ¬ ∃ 𝑧 ∈ ( 1 ..^ 𝐾 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑌 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
30 17 29 sylbid ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ¬ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
31 30 com12 ⊢ ( ¬ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
32 8 31 syl6com ⊢ ( ¬ ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ( 𝑌 = 0 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
33 3 32 sylbi ⊢ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ( 𝑌 = 0 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
34 33 adantr ⊢ ( ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) → ( 𝑌 = 0 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
35 34 com12 ⊢ ( 𝑌 = 0 → ( ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
36 df-nel ⊢ ( ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) )
37 fveq2 ⊢ ( 𝐾 = 𝑌 → ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ 𝑌 ) )
38 37 eqcoms ⊢ ( 𝑌 = 𝐾 → ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ 𝑌 ) )
39 38 eleq1d ⊢ ( 𝑌 = 𝐾 → ( ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
40 39 notbid ⊢ ( 𝑌 = 𝐾 → ( ¬ ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
41 40 biimpd ⊢ ( 𝑌 = 𝐾 → ( ¬ ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ¬ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
42 41 31 syl6com ⊢ ( ¬ ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ( 𝑌 = 𝐾 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
43 36 42 sylbi ⊢ ( ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) → ( 𝑌 = 𝐾 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
44 43 adantl ⊢ ( ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) → ( 𝑌 = 𝐾 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
45 44 com12 ⊢ ( 𝑌 = 𝐾 → ( ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
46 35 45 jaoi ⊢ ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
47 46 com13 ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
48 2 47 sylbid ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
49 48 com14 ⊢ ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
50 49 com12 ⊢ ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
51 50 com15 ⊢ ( 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
52 elfznelfzo ⊢ ( ( 𝑋 ∈ ( 0 ... 𝐾 ) ∧ ¬ 𝑋 ∈ ( 1 ..^ 𝐾 ) ) → ( 𝑋 = 0 ∨ 𝑋 = 𝐾 ) )
53 eqtr3 ⊢ ( ( 𝑋 = 0 ∧ 𝑌 = 0 ) → 𝑋 = 𝑌 )
54 2a1 ⊢ ( 𝑋 = 𝑌 → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
55 54 2a1d ⊢ ( 𝑋 = 𝑌 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
56 53 55 syl ⊢ ( ( 𝑋 = 0 ∧ 𝑌 = 0 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
57 5 adantl ⊢ ( ( 𝑋 = 𝐾 ∧ 𝑌 = 0 ) → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 𝑌 ) )
58 fveq2 ⊢ ( 𝐾 = 𝑋 → ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ 𝑋 ) )
59 58 eqcoms ⊢ ( 𝑋 = 𝐾 → ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ 𝑋 ) )
60 59 adantr ⊢ ( ( 𝑋 = 𝐾 ∧ 𝑌 = 0 ) → ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ 𝑋 ) )
61 57 60 neeq12d ⊢ ( ( 𝑋 = 𝐾 ∧ 𝑌 = 0 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) ↔ ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ) )
62 df-ne ⊢ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) ↔ ¬ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) )
63 pm2.24 ⊢ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → ( ¬ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑌 ) )
64 63 eqcoms ⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → ( ¬ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑌 ) )
65 64 com12 ⊢ ( ¬ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
66 62 65 sylbi ⊢ ( ( 𝐹 ‘ 𝑌 ) ≠ ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
67 61 66 syl6bi ⊢ ( ( 𝑋 = 𝐾 ∧ 𝑌 = 0 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
68 67 2a1d ⊢ ( ( 𝑋 = 𝐾 ∧ 𝑌 = 0 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
69 fveq2 ⊢ ( 0 = 𝑋 → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 𝑋 ) )
70 69 eqcoms ⊢ ( 𝑋 = 0 → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 𝑋 ) )
71 70 adantr ⊢ ( ( 𝑋 = 0 ∧ 𝑌 = 𝐾 ) → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 𝑋 ) )
72 38 adantl ⊢ ( ( 𝑋 = 0 ∧ 𝑌 = 𝐾 ) → ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ 𝑌 ) )
73 71 72 neeq12d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 = 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
74 df-ne ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ↔ ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
75 74 22 sylbi ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
76 73 75 syl6bi ⊢ ( ( 𝑋 = 0 ∧ 𝑌 = 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
77 76 2a1d ⊢ ( ( 𝑋 = 0 ∧ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
78 eqtr3 ⊢ ( ( 𝑋 = 𝐾 ∧ 𝑌 = 𝐾 ) → 𝑋 = 𝑌 )
79 78 55 syl ⊢ ( ( 𝑋 = 𝐾 ∧ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
80 56 68 77 79 ccase ⊢ ( ( ( 𝑋 = 0 ∨ 𝑋 = 𝐾 ) ∧ ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) )
81 80 ex ⊢ ( ( 𝑋 = 0 ∨ 𝑋 = 𝐾 ) → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
82 52 81 syl ⊢ ( ( 𝑋 ∈ ( 0 ... 𝐾 ) ∧ ¬ 𝑋 ∈ ( 1 ..^ 𝐾 ) ) → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
83 82 expcom ⊢ ( ¬ 𝑋 ∈ ( 1 ..^ 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
84 51 83 pm2.61i ⊢ ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
85 84 com12 ⊢ ( ( 𝑌 = 0 ∨ 𝑌 = 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
86 1 85 syl ⊢ ( ( 𝑌 ∈ ( 0 ... 𝐾 ) ∧ ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
87 86 ex ⊢ ( 𝑌 ∈ ( 0 ... 𝐾 ) → ( ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
88 87 com23 ⊢ ( 𝑌 ∈ ( 0 ... 𝐾 ) → ( 𝑋 ∈ ( 0 ... 𝐾 ) → ( ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) ) )
89 88 impcom ⊢ ( ( 𝑋 ∈ ( 0 ... 𝐾 ) ∧ 𝑌 ∈ ( 0 ... 𝐾 ) ) → ( ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
90 89 com12 ⊢ ( ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝑋 ∈ ( 0 ... 𝐾 ) ∧ 𝑌 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )
91 90 com25 ⊢ ( ¬ 𝑌 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑋 ∈ ( 0 ... 𝐾 ) ∧ 𝑌 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) ) ) )