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