Theorem updjudhf

Description: The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022)

	Ref	Expression
Hypotheses	updjud.f	$$⊢\phi \to F:A⟶C$$
	updjud.g	$$⊢\phi \to G:B⟶C$$
	updjudhf.h	$$⊢H=\left(x\in \left(A\mathrm{\bigsqcup ︀}B\right)⟼if\left(1^{st}\left(x\right)=\varnothing ,F\left(2^{nd}\left(x\right)\right),G\left(2^{nd}\left(x\right)\right)\right)\right)$$
Assertion	updjudhf	$$⊢\phi \to H:\left(A\mathrm{\bigsqcup ︀}B\right)⟶C$$

Proof

Step	Hyp	Ref	Expression
1		updjud.f	$$⊢\phi \to F:A⟶C$$
2		updjud.g	$$⊢\phi \to G:B⟶C$$
3		updjudhf.h	$$⊢H=\left(x\in \left(A\mathrm{\bigsqcup ︀}B\right)⟼if\left(1^{st}\left(x\right)=\varnothing ,F\left(2^{nd}\left(x\right)\right),G\left(2^{nd}\left(x\right)\right)\right)\right)$$
4		eldju2ndl	$$⊢\left(x\in \left(A\mathrm{\bigsqcup ︀}B\right)\wedge 1^{st}\left(x\right)=\varnothing \right)\to 2^{nd}\left(x\right)\in A$$
5	4	ex	$$⊢x\in \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(1^{st}\left(x\right)=\varnothing \to 2^{nd}\left(x\right)\in A\right)$$
6		ffvelrn	$$⊢\left(F:A⟶C\wedge 2^{nd}\left(x\right)\in A\right)\to F\left(2^{nd}\left(x\right)\right)\in C$$
7	6	ex	$$⊢F:A⟶C\to \left(2^{nd}\left(x\right)\in A\to F\left(2^{nd}\left(x\right)\right)\in C\right)$$
8	1 7	syl	$$⊢\phi \to \left(2^{nd}\left(x\right)\in A\to F\left(2^{nd}\left(x\right)\right)\in C\right)$$
9	5 8	sylan9r	$$⊢\left(\phi \wedge x\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to \left(1^{st}\left(x\right)=\varnothing \to F\left(2^{nd}\left(x\right)\right)\in C\right)$$
10	9	imp	$$⊢\left(\left(\phi \wedge x\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\wedge 1^{st}\left(x\right)=\varnothing \right)\to F\left(2^{nd}\left(x\right)\right)\in C$$
11		df-ne	$$⊢1^{st}\left(x\right)\ne \varnothing \leftrightarrow \neg 1^{st}\left(x\right)=\varnothing$$
12		eldju2ndr	$$⊢\left(x\in \left(A\mathrm{\bigsqcup ︀}B\right)\wedge 1^{st}\left(x\right)\ne \varnothing \right)\to 2^{nd}\left(x\right)\in B$$
13	12	ex	$$⊢x\in \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(1^{st}\left(x\right)\ne \varnothing \to 2^{nd}\left(x\right)\in B\right)$$
14		ffvelrn	$$⊢\left(G:B⟶C\wedge 2^{nd}\left(x\right)\in B\right)\to G\left(2^{nd}\left(x\right)\right)\in C$$
15	14	ex	$$⊢G:B⟶C\to \left(2^{nd}\left(x\right)\in B\to G\left(2^{nd}\left(x\right)\right)\in C\right)$$
16	2 15	syl	$$⊢\phi \to \left(2^{nd}\left(x\right)\in B\to G\left(2^{nd}\left(x\right)\right)\in C\right)$$
17	13 16	sylan9r	$$⊢\left(\phi \wedge x\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to \left(1^{st}\left(x\right)\ne \varnothing \to G\left(2^{nd}\left(x\right)\right)\in C\right)$$
18	11 17	syl5bir	$$⊢\left(\phi \wedge x\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to \left(\neg 1^{st}\left(x\right)=\varnothing \to G\left(2^{nd}\left(x\right)\right)\in C\right)$$
19	18	imp	$$⊢\left(\left(\phi \wedge x\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\wedge \neg 1^{st}\left(x\right)=\varnothing \right)\to G\left(2^{nd}\left(x\right)\right)\in C$$
20	10 19	ifclda	$$⊢\left(\phi \wedge x\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to if\left(1^{st}\left(x\right)=\varnothing ,F\left(2^{nd}\left(x\right)\right),G\left(2^{nd}\left(x\right)\right)\right)\in C$$
21	20 3	fmptd	$$⊢\phi \to H:\left(A\mathrm{\bigsqcup ︀}B\right)⟶C$$