Theorem bj-funun

Description: Value of a function expressed as a union of two functions at a point not in the domain of one of them. (Contributed by BJ, 18-Mar-2023)

	Ref	Expression
Hypotheses	bj-funun.un	|- ( ph -> F = ( G u. H ) )
	bj-funun.neldm	|- ( ph -> -. A e. dom H )
Assertion	bj-funun	|- ( ph -> ( F ` A ) = ( G ` A ) )

Proof

Step	Hyp	Ref	Expression
1		bj-funun.un	|- ( ph -> F = ( G u. H ) )
2		bj-funun.neldm	|- ( ph -> -. A e. dom H )
3		imaeq1	|- ( F = ( G u. H ) -> ( F " { A } ) = ( ( G u. H ) " { A } ) )
4		imaundir	|- ( ( G u. H ) " { A } ) = ( ( G " { A } ) u. ( H " { A } ) )
5	3 4	eqtrdi	|- ( F = ( G u. H ) -> ( F " { A } ) = ( ( G " { A } ) u. ( H " { A } ) ) )
6	1 5	syl	|- ( ph -> ( F " { A } ) = ( ( G " { A } ) u. ( H " { A } ) ) )
7		ndmima	|- ( -. A e. dom H -> ( H " { A } ) = (/) )
8	2 7	syl	|- ( ph -> ( H " { A } ) = (/) )
9		uneq2	|- ( ( H " { A } ) = (/) -> ( ( G " { A } ) u. ( H " { A } ) ) = ( ( G " { A } ) u. (/) ) )
10		un0	|- ( ( G " { A } ) u. (/) ) = ( G " { A } )
11	9 10	eqtrdi	|- ( ( H " { A } ) = (/) -> ( ( G " { A } ) u. ( H " { A } ) ) = ( G " { A } ) )
12	8 11	syl	|- ( ph -> ( ( G " { A } ) u. ( H " { A } ) ) = ( G " { A } ) )
13	6 12	eqtrd	|- ( ph -> ( F " { A } ) = ( G " { A } ) )
14		bj-imafv	|- ( ( F " { A } ) = ( G " { A } ) -> ( F ` A ) = ( G ` A ) )
15	13 14	syl	|- ( ph -> ( F ` A ) = ( G ` A ) )