Metamath Proof Explorer


Theorem resunimafz0

Description: TODO-AV: Revise using F e. Word dom I ? Formerly part of proof of eupth2lem3 : The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 20-Feb-2021)

Ref Expression
Hypotheses resunimafz0.i ( 𝜑 → Fun 𝐼 )
resunimafz0.f ( 𝜑𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
resunimafz0.n ( 𝜑𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
Assertion resunimafz0 ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ { ⟨ ( 𝐹𝑁 ) , ( 𝐼 ‘ ( 𝐹𝑁 ) ) ⟩ } ) )

Proof

Step Hyp Ref Expression
1 resunimafz0.i ( 𝜑 → Fun 𝐼 )
2 resunimafz0.f ( 𝜑𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
3 resunimafz0.n ( 𝜑𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
4 imaundi ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ) = ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ∪ ( 𝐹 “ { 𝑁 } ) )
5 elfzonn0 ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑁 ∈ ℕ0 )
6 3 5 syl ( 𝜑𝑁 ∈ ℕ0 )
7 elnn0uz ( 𝑁 ∈ ℕ0𝑁 ∈ ( ℤ ‘ 0 ) )
8 6 7 sylib ( 𝜑𝑁 ∈ ( ℤ ‘ 0 ) )
9 fzisfzounsn ( 𝑁 ∈ ( ℤ ‘ 0 ) → ( 0 ... 𝑁 ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
10 8 9 syl ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
11 10 imaeq2d ( 𝜑 → ( 𝐹 “ ( 0 ... 𝑁 ) ) = ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ) )
12 2 ffnd ( 𝜑𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
13 fnsnfv ( ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → { ( 𝐹𝑁 ) } = ( 𝐹 “ { 𝑁 } ) )
14 12 3 13 syl2anc ( 𝜑 → { ( 𝐹𝑁 ) } = ( 𝐹 “ { 𝑁 } ) )
15 14 uneq2d ( 𝜑 → ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ∪ { ( 𝐹𝑁 ) } ) = ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ∪ ( 𝐹 “ { 𝑁 } ) ) )
16 4 11 15 3eqtr4a ( 𝜑 → ( 𝐹 “ ( 0 ... 𝑁 ) ) = ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ∪ { ( 𝐹𝑁 ) } ) )
17 16 reseq2d ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) = ( 𝐼 ↾ ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ∪ { ( 𝐹𝑁 ) } ) ) )
18 resundi ( 𝐼 ↾ ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ∪ { ( 𝐹𝑁 ) } ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ ( 𝐼 ↾ { ( 𝐹𝑁 ) } ) )
19 17 18 syl6eq ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ ( 𝐼 ↾ { ( 𝐹𝑁 ) } ) ) )
20 1 funfnd ( 𝜑𝐼 Fn dom 𝐼 )
21 2 3 ffvelrnd ( 𝜑 → ( 𝐹𝑁 ) ∈ dom 𝐼 )
22 fnressn ( ( 𝐼 Fn dom 𝐼 ∧ ( 𝐹𝑁 ) ∈ dom 𝐼 ) → ( 𝐼 ↾ { ( 𝐹𝑁 ) } ) = { ⟨ ( 𝐹𝑁 ) , ( 𝐼 ‘ ( 𝐹𝑁 ) ) ⟩ } )
23 20 21 22 syl2anc ( 𝜑 → ( 𝐼 ↾ { ( 𝐹𝑁 ) } ) = { ⟨ ( 𝐹𝑁 ) , ( 𝐼 ‘ ( 𝐹𝑁 ) ) ⟩ } )
24 23 uneq2d ( 𝜑 → ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ ( 𝐼 ↾ { ( 𝐹𝑁 ) } ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ { ⟨ ( 𝐹𝑁 ) , ( 𝐼 ‘ ( 𝐹𝑁 ) ) ⟩ } ) )
25 19 24 eqtrd ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ { ⟨ ( 𝐹𝑁 ) , ( 𝐼 ‘ ( 𝐹𝑁 ) ) ⟩ } ) )