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 ◡ 𝐹 ) ) )