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) (Revised by Mingli Yuan, 15-Aug-2026)

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