Theorem updjudhcoinlf

Description: The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-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	updjudhcoinlf	$$⊢\phi \to H\circ \left({inl\upharpoonright }_A\right)=F$$

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	1 2 3	updjudhf	$$⊢\phi \to H:\left(A\mathrm{\bigsqcup ︀}B\right)⟶C$$
5	4	ffnd	$$⊢\phi \to HFn\left(A\mathrm{\bigsqcup ︀}B\right)$$
6		inlresf	$$⊢\left({inl\upharpoonright }_A\right):A⟶\left(A\mathrm{\bigsqcup ︀}B\right)$$
7		ffn	$$⊢\left({inl\upharpoonright }_A\right):A⟶\left(A\mathrm{\bigsqcup ︀}B\right)\to \left({inl\upharpoonright }_A\right)FnA$$
8	6 7	mp1i	$$⊢\phi \to \left({inl\upharpoonright }_A\right)FnA$$
9		frn	$$⊢\left({inl\upharpoonright }_A\right):A⟶\left(A\mathrm{\bigsqcup ︀}B\right)\to \mathrm{ran}\left({inl\upharpoonright }_A\right)\subseteq \left(A\mathrm{\bigsqcup ︀}B\right)$$
10	6 9	mp1i	$$⊢\phi \to \mathrm{ran}\left({inl\upharpoonright }_A\right)\subseteq \left(A\mathrm{\bigsqcup ︀}B\right)$$
11		fnco	$$⊢\left(HFn\left(A\mathrm{\bigsqcup ︀}B\right)\wedge \left({inl\upharpoonright }_A\right)FnA\wedge \mathrm{ran}\left({inl\upharpoonright }_A\right)\subseteq \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to \left(H\circ \left({inl\upharpoonright }_A\right)\right)FnA$$
12	5 8 10 11	syl3anc	$$⊢\phi \to \left(H\circ \left({inl\upharpoonright }_A\right)\right)FnA$$
13	1	ffnd	$$⊢\phi \to FFnA$$
14		fvco2	$$⊢\left(\left({inl\upharpoonright }_A\right)FnA\wedge a\in A\right)\to \left(H\circ \left({inl\upharpoonright }_A\right)\right)\left(a\right)=H\left(\left({inl\upharpoonright }_A\right)\left(a\right)\right)$$
15	8 14	sylan	$$⊢\left(\phi \wedge a\in A\right)\to \left(H\circ \left({inl\upharpoonright }_A\right)\right)\left(a\right)=H\left(\left({inl\upharpoonright }_A\right)\left(a\right)\right)$$
16		fvres	$$⊢a\in A\to \left({inl\upharpoonright }_A\right)\left(a\right)=inl\left(a\right)$$
17	16	adantl	$$⊢\left(\phi \wedge a\in A\right)\to \left({inl\upharpoonright }_A\right)\left(a\right)=inl\left(a\right)$$
18	17	fveq2d	$$⊢\left(\phi \wedge a\in A\right)\to H\left(\left({inl\upharpoonright }_A\right)\left(a\right)\right)=H\left(inl\left(a\right)\right)$$
19		fveqeq2	$$⊢x=inl\left(a\right)\to \left(1^{st}\left(x\right)=\varnothing \leftrightarrow 1^{st}\left(inl\left(a\right)\right)=\varnothing \right)$$
20		2fveq3	$$⊢x=inl\left(a\right)\to F\left(2^{nd}\left(x\right)\right)=F\left(2^{nd}\left(inl\left(a\right)\right)\right)$$
21		2fveq3	$$⊢x=inl\left(a\right)\to G\left(2^{nd}\left(x\right)\right)=G\left(2^{nd}\left(inl\left(a\right)\right)\right)$$
22	19 20 21	ifbieq12d	$$⊢x=inl\left(a\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)=if\left(1^{st}\left(inl\left(a\right)\right)=\varnothing ,F\left(2^{nd}\left(inl\left(a\right)\right)\right),G\left(2^{nd}\left(inl\left(a\right)\right)\right)\right)$$
23	22	adantl	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge x=inl\left(a\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)=if\left(1^{st}\left(inl\left(a\right)\right)=\varnothing ,F\left(2^{nd}\left(inl\left(a\right)\right)\right),G\left(2^{nd}\left(inl\left(a\right)\right)\right)\right)$$
24		1stinl	$$⊢a\in A\to 1^{st}\left(inl\left(a\right)\right)=\varnothing$$
25	24	adantl	$$⊢\left(\phi \wedge a\in A\right)\to 1^{st}\left(inl\left(a\right)\right)=\varnothing$$
26	25	adantr	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge x=inl\left(a\right)\right)\to 1^{st}\left(inl\left(a\right)\right)=\varnothing$$
27	26	iftrued	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge x=inl\left(a\right)\right)\to if\left(1^{st}\left(inl\left(a\right)\right)=\varnothing ,F\left(2^{nd}\left(inl\left(a\right)\right)\right),G\left(2^{nd}\left(inl\left(a\right)\right)\right)\right)=F\left(2^{nd}\left(inl\left(a\right)\right)\right)$$
28	23 27	eqtrd	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge x=inl\left(a\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)=F\left(2^{nd}\left(inl\left(a\right)\right)\right)$$
29		djulcl	$$⊢a\in A\to inl\left(a\right)\in \left(A\mathrm{\bigsqcup ︀}B\right)$$
30	29	adantl	$$⊢\left(\phi \wedge a\in A\right)\to inl\left(a\right)\in \left(A\mathrm{\bigsqcup ︀}B\right)$$
31	1	adantr	$$⊢\left(\phi \wedge a\in A\right)\to F:A⟶C$$
32		2ndinl	$$⊢a\in A\to 2^{nd}\left(inl\left(a\right)\right)=a$$
33	32	adantl	$$⊢\left(\phi \wedge a\in A\right)\to 2^{nd}\left(inl\left(a\right)\right)=a$$
34		simpr	$$⊢\left(\phi \wedge a\in A\right)\to a\in A$$
35	33 34	eqeltrd	$$⊢\left(\phi \wedge a\in A\right)\to 2^{nd}\left(inl\left(a\right)\right)\in A$$
36	31 35	ffvelrnd	$$⊢\left(\phi \wedge a\in A\right)\to F\left(2^{nd}\left(inl\left(a\right)\right)\right)\in C$$
37	3 28 30 36	fvmptd2	$$⊢\left(\phi \wedge a\in A\right)\to H\left(inl\left(a\right)\right)=F\left(2^{nd}\left(inl\left(a\right)\right)\right)$$
38	18 37	eqtrd	$$⊢\left(\phi \wedge a\in A\right)\to H\left(\left({inl\upharpoonright }_A\right)\left(a\right)\right)=F\left(2^{nd}\left(inl\left(a\right)\right)\right)$$
39	33	fveq2d	$$⊢\left(\phi \wedge a\in A\right)\to F\left(2^{nd}\left(inl\left(a\right)\right)\right)=F\left(a\right)$$
40	15 38 39	3eqtrd	$$⊢\left(\phi \wedge a\in A\right)\to \left(H\circ \left({inl\upharpoonright }_A\right)\right)\left(a\right)=F\left(a\right)$$
41	12 13 40	eqfnfvd	$$⊢\phi \to H\circ \left({inl\upharpoonright }_A\right)=F$$