This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrdi ⊢ ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ ( 𝐼 ↾ { ( 𝐹 ‘ 𝑁 ) } ) ) )
20 1 funfnd ⊢ ( 𝜑 → 𝐼 Fn dom 𝐼 )
21 2 3 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ dom 𝐼 )
22 fnressn ⊢ ( ( 𝐼 Fn dom 𝐼 ∧ ( 𝐹 ‘ 𝑁 ) ∈ dom 𝐼 ) → ( 𝐼 ↾ { ( 𝐹 ‘ 𝑁 ) } ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
23 20 21 22 syl2anc ⊢ ( 𝜑 → ( 𝐼 ↾ { ( 𝐹 ‘ 𝑁 ) } ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
24 23 uneq2d ⊢ ( 𝜑 → ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ ( 𝐼 ↾ { ( 𝐹 ‘ 𝑁 ) } ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ) )
25 19 24 eqtrd ⊢ ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) = ( ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∪ { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ) )