Metamath Proof Explorer


Theorem injresinj

Description: A function whose restriction is injective and the values of the remaining arguments are different from all other values is injective itself. (Contributed by Alexander van der Vekens, 31-Oct-2017)

Ref Expression
Assertion injresinj ( 𝐾 ∈ ℕ0 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → Fun 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 fzo0ss1 ( 1 ..^ 𝐾 ) ⊆ ( 0 ..^ 𝐾 )
2 fzossfz ( 0 ..^ 𝐾 ) ⊆ ( 0 ... 𝐾 )
3 1 2 sstri ( 1 ..^ 𝐾 ) ⊆ ( 0 ... 𝐾 )
4 fssres ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ ( 1 ..^ 𝐾 ) ⊆ ( 0 ... 𝐾 ) ) → ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 )
5 3 4 mpan2 ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 )
6 5 biantrud ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ↔ ( Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 ) ) )
7 ancom ( ( Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 ) ↔ ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 ∧ Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ) )
8 df-f1 ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 ↔ ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 ∧ Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ) )
9 7 8 bitr4i ( ( Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 ) ↔ ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 )
10 6 9 bitrdi ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ↔ ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 ) )
11 simp-4r ( ( ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 )
12 dff13 ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 ↔ ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) ⟶ 𝑉 ∧ ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
13 fveqeq2 ( 𝑣 = 𝑥 → ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) ↔ ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) ) )
14 equequ1 ( 𝑣 = 𝑥 → ( 𝑣 = 𝑤𝑥 = 𝑤 ) )
15 13 14 imbi12d ( 𝑣 = 𝑥 → ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ↔ ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑥 = 𝑤 ) ) )
16 fveq2 ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) )
17 16 eqeq2d ( 𝑤 = 𝑦 → ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) ↔ ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) ) )
18 equequ2 ( 𝑤 = 𝑦 → ( 𝑥 = 𝑤𝑥 = 𝑦 ) )
19 17 18 imbi12d ( 𝑤 = 𝑦 → ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑥 = 𝑤 ) ↔ ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
20 15 19 rspc2va ( ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) ∧ ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) → ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
21 fvres ( 𝑥 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
22 21 eqcomd ( 𝑥 ∈ ( 1 ..^ 𝐾 ) → ( 𝐹𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) )
23 fvres ( 𝑦 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) = ( 𝐹𝑦 ) )
24 23 eqcomd ( 𝑦 ∈ ( 1 ..^ 𝐾 ) → ( 𝐹𝑦 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) )
25 22 24 eqeqan12d ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ↔ ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) ) )
26 25 biimpd ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) ) )
27 26 imim1d ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
28 27 imp ( ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) ∧ ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) )
29 28 2a1d ( ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) ∧ ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) )
30 29 2a1d ( ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) ∧ ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
31 30 expcom ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) → ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) ) )
32 20 31 syl ( ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) ∧ ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) → ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) ) )
33 32 ex ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) → ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) ) ) )
34 33 pm2.43a ( ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) ) )
35 ianor ( ¬ ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) ↔ ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∨ ¬ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) )
36 eqcom ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ↔ ( 𝐹𝑦 ) = ( 𝐹𝑥 ) )
37 injresinjlem ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑦 ∈ ( 0 ... 𝐾 ) ∧ 𝑥 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑦 ) = ( 𝐹𝑥 ) → 𝑦 = 𝑥 ) ) ) ) ) )
38 37 imp ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑦 ∈ ( 0 ... 𝐾 ) ∧ 𝑥 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑦 ) = ( 𝐹𝑥 ) → 𝑦 = 𝑥 ) ) ) ) )
39 38 imp41 ( ( ( ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) ∧ ( 𝑦 ∈ ( 0 ... 𝐾 ) ∧ 𝑥 ∈ ( 0 ... 𝐾 ) ) ) → ( ( 𝐹𝑦 ) = ( 𝐹𝑥 ) → 𝑦 = 𝑥 ) )
40 eqcom ( 𝑦 = 𝑥𝑥 = 𝑦 )
41 39 40 syl6ib ( ( ( ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) ∧ ( 𝑦 ∈ ( 0 ... 𝐾 ) ∧ 𝑥 ∈ ( 0 ... 𝐾 ) ) ) → ( ( 𝐹𝑦 ) = ( 𝐹𝑥 ) → 𝑥 = 𝑦 ) )
42 36 41 syl5bi ( ( ( ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) ∧ ( 𝑦 ∈ ( 0 ... 𝐾 ) ∧ 𝑥 ∈ ( 0 ... 𝐾 ) ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) )
43 42 ex ( ( ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → ( ( 𝑦 ∈ ( 0 ... 𝐾 ) ∧ 𝑥 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
44 43 ancomsd ( ( ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
45 44 exp41 ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
46 injresinjlem ( ¬ 𝑦 ∈ ( 1 ..^ 𝐾 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
47 45 46 jaoi ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∨ ¬ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
48 47 a1d ( ( ¬ 𝑥 ∈ ( 1 ..^ 𝐾 ) ∨ ¬ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) ) )
49 35 48 sylbi ( ¬ ( 𝑥 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑦 ∈ ( 1 ..^ 𝐾 ) ) → ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) ) )
50 34 49 pm2.61i ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
51 50 imp41 ( ( ( ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → ( ( 𝑥 ∈ ( 0 ... 𝐾 ) ∧ 𝑦 ∈ ( 0 ... 𝐾 ) ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
52 51 ralrimivv ( ( ( ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) )
53 52 exp41 ( ∀ 𝑣 ∈ ( 1 ..^ 𝐾 ) ∀ 𝑤 ∈ ( 1 ..^ 𝐾 ) ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑣 ) = ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
54 12 53 simplbiim ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
55 54 com13 ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉𝐾 ∈ ℕ0 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
56 55 ex ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( 𝐾 ∈ ℕ0 → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
57 56 com24 ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( 𝐾 ∈ ℕ0 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
58 57 impcom ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( 𝐾 ∈ ℕ0 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
59 58 imp41 ( ( ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) )
60 dff13 ( 𝐹 : ( 0 ... 𝐾 ) –1-1𝑉 ↔ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ ∀ 𝑥 ∈ ( 0 ... 𝐾 ) ∀ 𝑦 ∈ ( 0 ... 𝐾 ) ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
61 11 59 60 sylanbrc ( ( ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → 𝐹 : ( 0 ... 𝐾 ) –1-1𝑉 )
62 11 biantrurd ( ( ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → ( Fun 𝐹 ↔ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ Fun 𝐹 ) ) )
63 df-f1 ( 𝐹 : ( 0 ... 𝐾 ) –1-1𝑉 ↔ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ Fun 𝐹 ) )
64 62 63 bitr4di ( ( ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → ( Fun 𝐹𝐹 : ( 0 ... 𝐾 ) –1-1𝑉 ) )
65 61 64 mpbird ( ( ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ 𝐾 ∈ ℕ0 ) ∧ ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) → Fun 𝐹 )
66 65 ex ( ( ( ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → Fun 𝐹 ) )
67 66 exp41 ( ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) : ( 1 ..^ 𝐾 ) –1-1𝑉 → ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( 𝐾 ∈ ℕ0 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → Fun 𝐹 ) ) ) ) )
68 10 67 syl6bi ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) → ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( 𝐾 ∈ ℕ0 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → Fun 𝐹 ) ) ) ) ) )
69 68 pm2.43a ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → ( Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) → ( 𝐾 ∈ ℕ0 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → Fun 𝐹 ) ) ) ) )
70 69 3imp ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) → ( 𝐾 ∈ ℕ0 → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → Fun 𝐹 ) ) )
71 70 com12 ( 𝐾 ∈ ℕ0 → ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ Fun ( 𝐹 ↾ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹𝐾 ) ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ → Fun 𝐹 ) ) )