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