Metamath Proof Explorer

Theorem f1resfz0f1d

Description: If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023)

Ref Expression
Hypotheses f1resfz0f1d.1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
f1resfz0f1d.2 ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 )
f1resfz0f1d.3 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 1 ... 𝐾 ) ) : ( 1 ... 𝐾 ) –1-1→ 𝑉 )
f1resfz0f1d.4 ⊢ ( 𝜑 → ( ( 𝐹 “ { 0 } ) ∩ ( 𝐹 “ ( 1 ... 𝐾 ) ) ) = ∅ )
Assertion f1resfz0f1d ( 𝜑 → 𝐹 : ( 0 ... 𝐾 ) –1-1→ 𝑉 )

Proof

Step Hyp Ref Expression
1 f1resfz0f1d.1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
2 f1resfz0f1d.2 ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐾 ) ⟶ 𝑉 )
3 f1resfz0f1d.3 ⊢ ( 𝜑 → ( 𝐹 ↾ ( 1 ... 𝐾 ) ) : ( 1 ... 𝐾 ) –1-1→ 𝑉 )
4 f1resfz0f1d.4 ⊢ ( 𝜑 → ( ( 𝐹 “ { 0 } ) ∩ ( 𝐹 “ ( 1 ... 𝐾 ) ) ) = ∅ )
5 fz1ssfz0 ⊢ ( 1 ... 𝐾 ) ⊆ ( 0 ... 𝐾 )
6 5 a1i ⊢ ( 𝜑 → ( 1 ... 𝐾 ) ⊆ ( 0 ... 𝐾 ) )
7 0elfz ⊢ ( 𝐾 ∈ ℕ0 → 0 ∈ ( 0 ... 𝐾 ) )
8 snssi ⊢ ( 0 ∈ ( 0 ... 𝐾 ) → { 0 } ⊆ ( 0 ... 𝐾 ) )
9 1 7 8 3syl ⊢ ( 𝜑 → { 0 } ⊆ ( 0 ... 𝐾 ) )
10 2 9 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ { 0 } ) : { 0 } ⟶ 𝑉 )
11 eqidd ⊢ ( ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) → 0 = 0 )
12 0nn0 ⊢ 0 ∈ ℕ0
13 fveqeq2 ⊢ ( 𝑥 = 0 → ( ( ( 𝐹 ↾ { 0 } ) ‘ 𝑥 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) ↔ ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) ) )
14 eqeq1 ⊢ ( 𝑥 = 0 → ( 𝑥 = 𝑦 ↔ 0 = 𝑦 ) )
15 13 14 imbi12d ⊢ ( 𝑥 = 0 → ( ( ( ( 𝐹 ↾ { 0 } ) ‘ 𝑥 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) → 0 = 𝑦 ) ) )
16 fveq2 ⊢ ( 𝑦 = 0 → ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) )
17 16 eqeq2d ⊢ ( 𝑦 = 0 → ( ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) ↔ ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) ) )
18 eqeq2 ⊢ ( 𝑦 = 0 → ( 0 = 𝑦 ↔ 0 = 0 ) )
19 17 18 imbi12d ⊢ ( 𝑦 = 0 → ( ( ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) → 0 = 𝑦 ) ↔ ( ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) → 0 = 0 ) ) )
20 15 19 2ralsng ⊢ ( ( 0 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( ( 𝐹 ↾ { 0 } ) ‘ 𝑥 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) → 0 = 0 ) ) )
21 12 12 20 mp2an ⊢ ( ∀ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( ( 𝐹 ↾ { 0 } ) ‘ 𝑥 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 0 ) → 0 = 0 ) )
22 11 21 mpbir ⊢ ∀ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( ( 𝐹 ↾ { 0 } ) ‘ 𝑥 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) → 𝑥 = 𝑦 )
23 dff13 ⊢ ( ( 𝐹 ↾ { 0 } ) : { 0 } –1-1→ 𝑉 ↔ ( ( 𝐹 ↾ { 0 } ) : { 0 } ⟶ 𝑉 ∧ ∀ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( ( 𝐹 ↾ { 0 } ) ‘ 𝑥 ) = ( ( 𝐹 ↾ { 0 } ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
24 10 22 23 sylanblrc ⊢ ( 𝜑 → ( 𝐹 ↾ { 0 } ) : { 0 } –1-1→ 𝑉 )
25 uncom ⊢ ( ( 1 ... 𝐾 ) ∪ { 0 } ) = ( { 0 } ∪ ( 1 ... 𝐾 ) )
26 fz0sn0fz1 ⊢ ( 𝐾 ∈ ℕ0 → ( 0 ... 𝐾 ) = ( { 0 } ∪ ( 1 ... 𝐾 ) ) )
27 1 26 syl ⊢ ( 𝜑 → ( 0 ... 𝐾 ) = ( { 0 } ∪ ( 1 ... 𝐾 ) ) )
28 25 27 eqtr4id ⊢ ( 𝜑 → ( ( 1 ... 𝐾 ) ∪ { 0 } ) = ( 0 ... 𝐾 ) )
29 0nelfz1 ⊢ 0 ∉ ( 1 ... 𝐾 )
30 29 neli ⊢ ¬ 0 ∈ ( 1 ... 𝐾 )
31 disjsn ⊢ ( ( ( 1 ... 𝐾 ) ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ( 1 ... 𝐾 ) )
32 30 31 mpbir ⊢ ( ( 1 ... 𝐾 ) ∩ { 0 } ) = ∅
33 uneqdifeq ⊢ ( ( ( 1 ... 𝐾 ) ⊆ ( 0 ... 𝐾 ) ∧ ( ( 1 ... 𝐾 ) ∩ { 0 } ) = ∅ ) → ( ( ( 1 ... 𝐾 ) ∪ { 0 } ) = ( 0 ... 𝐾 ) ↔ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) = { 0 } ) )
34 5 32 33 mp2an ⊢ ( ( ( 1 ... 𝐾 ) ∪ { 0 } ) = ( 0 ... 𝐾 ) ↔ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) = { 0 } )
35 28 34 sylib ⊢ ( 𝜑 → ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) = { 0 } )
36 35 eqcomd ⊢ ( 𝜑 → { 0 } = ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) )
37 36 reseq2d ⊢ ( 𝜑 → ( 𝐹 ↾ { 0 } ) = ( 𝐹 ↾ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) ) )
38 eqidd ⊢ ( 𝜑 → 𝑉 = 𝑉 )
39 37 36 38 f1eq123d ⊢ ( 𝜑 → ( ( 𝐹 ↾ { 0 } ) : { 0 } –1-1→ 𝑉 ↔ ( 𝐹 ↾ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) ) : ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) –1-1→ 𝑉 ) )
40 24 39 mpbid ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) ) : ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) –1-1→ 𝑉 )
41 36 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ { 0 } ) = ( 𝐹 “ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) ) )
42 41 ineq2d ⊢ ( 𝜑 → ( ( 𝐹 “ ( 1 ... 𝐾 ) ) ∩ ( 𝐹 “ { 0 } ) ) = ( ( 𝐹 “ ( 1 ... 𝐾 ) ) ∩ ( 𝐹 “ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) ) ) )
43 incom ⊢ ( ( 𝐹 “ { 0 } ) ∩ ( 𝐹 “ ( 1 ... 𝐾 ) ) ) = ( ( 𝐹 “ ( 1 ... 𝐾 ) ) ∩ ( 𝐹 “ { 0 } ) )
44 43 4 syl5eqr ⊢ ( 𝜑 → ( ( 𝐹 “ ( 1 ... 𝐾 ) ) ∩ ( 𝐹 “ { 0 } ) ) = ∅ )
45 42 44 eqtr3d ⊢ ( 𝜑 → ( ( 𝐹 “ ( 1 ... 𝐾 ) ) ∩ ( 𝐹 “ ( ( 0 ... 𝐾 ) ∖ ( 1 ... 𝐾 ) ) ) ) = ∅ )
46 6 2 3 40 45 f1resrcmplf1d ⊢ ( 𝜑 → 𝐹 : ( 0 ... 𝐾 ) –1-1→ 𝑉 )