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	⊢ ( 𝜑 → 𝐹 = ( 𝐺 ∪ 𝐻 ) )
	bj-funun.neldm	⊢ ( 𝜑 → ¬ 𝐴 ∈ dom 𝐻 )
Assertion	bj-funun	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-funun.un	⊢ ( 𝜑 → 𝐹 = ( 𝐺 ∪ 𝐻 ) )
2		bj-funun.neldm	⊢ ( 𝜑 → ¬ 𝐴 ∈ dom 𝐻 )
3		imaeq1	⊢ ( 𝐹 = ( 𝐺 ∪ 𝐻 ) → ( 𝐹 “ { 𝐴 } ) = ( ( 𝐺 ∪ 𝐻 ) “ { 𝐴 } ) )
4		imaundir	⊢ ( ( 𝐺 ∪ 𝐻 ) “ { 𝐴 } ) = ( ( 𝐺 “ { 𝐴 } ) ∪ ( 𝐻 “ { 𝐴 } ) )
5	3 4	eqtrdi	⊢ ( 𝐹 = ( 𝐺 ∪ 𝐻 ) → ( 𝐹 “ { 𝐴 } ) = ( ( 𝐺 “ { 𝐴 } ) ∪ ( 𝐻 “ { 𝐴 } ) ) )
6	1 5	syl	⊢ ( 𝜑 → ( 𝐹 “ { 𝐴 } ) = ( ( 𝐺 “ { 𝐴 } ) ∪ ( 𝐻 “ { 𝐴 } ) ) )
7		ndmima	⊢ ( ¬ 𝐴 ∈ dom 𝐻 → ( 𝐻 “ { 𝐴 } ) = ∅ )
8	2 7	syl	⊢ ( 𝜑 → ( 𝐻 “ { 𝐴 } ) = ∅ )
9		uneq2	⊢ ( ( 𝐻 “ { 𝐴 } ) = ∅ → ( ( 𝐺 “ { 𝐴 } ) ∪ ( 𝐻 “ { 𝐴 } ) ) = ( ( 𝐺 “ { 𝐴 } ) ∪ ∅ ) )
10		un0	⊢ ( ( 𝐺 “ { 𝐴 } ) ∪ ∅ ) = ( 𝐺 “ { 𝐴 } )
11	9 10	eqtrdi	⊢ ( ( 𝐻 “ { 𝐴 } ) = ∅ → ( ( 𝐺 “ { 𝐴 } ) ∪ ( 𝐻 “ { 𝐴 } ) ) = ( 𝐺 “ { 𝐴 } ) )
12	8 11	syl	⊢ ( 𝜑 → ( ( 𝐺 “ { 𝐴 } ) ∪ ( 𝐻 “ { 𝐴 } ) ) = ( 𝐺 “ { 𝐴 } ) )
13	6 12	eqtrd	⊢ ( 𝜑 → ( 𝐹 “ { 𝐴 } ) = ( 𝐺 “ { 𝐴 } ) )
14		bj-imafv	⊢ ( ( 𝐹 “ { 𝐴 } ) = ( 𝐺 “ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
15	13 14	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )