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	$$⊢\phi \to F=G\cup H$$
	bj-funun.neldm	$$⊢\phi \to \neg A\in \mathrm{dom}H$$
Assertion	bj-funun	$$⊢\phi \to F\left(A\right)=G\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-funun.un	$$⊢\phi \to F=G\cup H$$
2		bj-funun.neldm	$$⊢\phi \to \neg A\in \mathrm{dom}H$$
3		imaeq1	$$⊢F=G\cup H\to F\left[\left\{A\right\}\right]=\left(G\cup H\right)\left[\left\{A\right\}\right]$$
4		imaundir	$$⊢\left(G\cup H\right)\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]\cup H\left[\left\{A\right\}\right]$$
5	3 4	eqtrdi	$$⊢F=G\cup H\to F\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]\cup H\left[\left\{A\right\}\right]$$
6	1 5	syl	$$⊢\phi \to F\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]\cup H\left[\left\{A\right\}\right]$$
7		ndmima	$$⊢\neg A\in \mathrm{dom}H\to H\left[\left\{A\right\}\right]=\varnothing$$
8	2 7	syl	$$⊢\phi \to H\left[\left\{A\right\}\right]=\varnothing$$
9		uneq2	$$⊢H\left[\left\{A\right\}\right]=\varnothing \to G\left[\left\{A\right\}\right]\cup H\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]\cup \varnothing$$
10		un0	$$⊢G\left[\left\{A\right\}\right]\cup \varnothing =G\left[\left\{A\right\}\right]$$
11	9 10	eqtrdi	$$⊢H\left[\left\{A\right\}\right]=\varnothing \to G\left[\left\{A\right\}\right]\cup H\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]$$
12	8 11	syl	$$⊢\phi \to G\left[\left\{A\right\}\right]\cup H\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]$$
13	6 12	eqtrd	$$⊢\phi \to F\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]$$
14		bj-imafv	$$⊢F\left[\left\{A\right\}\right]=G\left[\left\{A\right\}\right]\to F\left(A\right)=G\left(A\right)$$
15	13 14	syl	$$⊢\phi \to F\left(A\right)=G\left(A\right)$$