Metamath Proof Explorer

Theorem fvinim0ffz

Description: The function values for the borders of a finite interval of integers, which is the domain of the function, are not in the image of the interior of the interval iff the intersection of the images of the interior and the borders is empty. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 5-Feb-2021)

Ref Expression
Assertion fvinim0ffz ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ↔ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 → 𝐹 Fn ( 0 ... 𝐾 ) )
2 1 adantr ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 𝐹 Fn ( 0 ... 𝐾 ) )
3 0nn0 ⊢ 0 ∈ ℕ0
4 3 a1i ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 0 ∈ ℕ0 )
5 simpr ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
6 nn0ge0 ⊢ ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
7 6 adantl ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 0 ≤ 𝐾 )
8 elfz2nn0 ⊢ ( 0 ∈ ( 0 ... 𝐾 ) ↔ ( 0 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 0 ≤ 𝐾 ) )
9 4 5 7 8 syl3anbrc ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 0 ∈ ( 0 ... 𝐾 ) )
10 id ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℕ0 )
11 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
12 11 leidd ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ≤ 𝐾 )
13 elfz2nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝐾 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝐾 ) )
14 10 10 12 13 syl3anbrc ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ( 0 ... 𝐾 ) )
15 14 adantl ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ( 0 ... 𝐾 ) )
16 fnimapr ⊢ ( ( 𝐹 Fn ( 0 ... 𝐾 ) ∧ 0 ∈ ( 0 ... 𝐾 ) ∧ 𝐾 ∈ ( 0 ... 𝐾 ) ) → ( 𝐹 “ { 0 , 𝐾 } ) = { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } )
17 2 9 15 16 syl3anc ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐹 “ { 0 , 𝐾 } ) = { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } )
18 17 ineq1d ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
19 18 eqeq1d ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ↔ ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ) )
20 disj ⊢ ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ↔ ∀ 𝑣 ∈ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } ¬ 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) )
21 fvex ⊢ ( 𝐹 ‘ 0 ) ∈ V
22 fvex ⊢ ( 𝐹 ‘ 𝐾 ) ∈ V
23 eleq1 ⊢ ( 𝑣 = ( 𝐹 ‘ 0 ) → ( 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
24 23 notbid ⊢ ( 𝑣 = ( 𝐹 ‘ 0 ) → ( ¬ 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
25 df-nel ⊢ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 0 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) )
26 24 25 bitr4di ⊢ ( 𝑣 = ( 𝐹 ‘ 0 ) → ( ¬ 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
27 eleq1 ⊢ ( 𝑣 = ( 𝐹 ‘ 𝐾 ) → ( 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
28 27 notbid ⊢ ( 𝑣 = ( 𝐹 ‘ 𝐾 ) → ( ¬ 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
29 df-nel ⊢ ( ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ¬ ( 𝐹 ‘ 𝐾 ) ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) )
30 28 29 bitr4di ⊢ ( 𝑣 = ( 𝐹 ‘ 𝐾 ) → ( ¬ 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
31 21 22 26 30 ralpr ⊢ ( ∀ 𝑣 ∈ { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } ¬ 𝑣 ∈ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ↔ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
32 20 31 bitri ⊢ ( ( { ( 𝐹 ‘ 0 ) , ( 𝐹 ‘ 𝐾 ) } ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ↔ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) )
33 19 32 bitrdi ⊢ ( ( 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( 𝐹 “ { 0 , 𝐾 } ) ∩ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) = ∅ ↔ ( ( 𝐹 ‘ 0 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝐾 ) ∉ ( 𝐹 “ ( 1 ..^ 𝐾 ) ) ) ) )