Theorem elmapresaunres2

Description: fresaunres2 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014)

	Ref	Expression
Assertion	elmapresaunres2	$$⊢\left(F\in \left(C^A\right)\wedge G\in \left(C^B\right)\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to {\left(F\cup G\right)\upharpoonright }_B=G$$

Proof

Step	Hyp	Ref	Expression
1		elmapi	$$⊢F\in \left(C^A\right)\to F:A⟶C$$
2		elmapi	$$⊢G\in \left(C^B\right)\to G:B⟶C$$
3		id	$$⊢{F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\to {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}$$
4		fresaunres2	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to {\left(F\cup G\right)\upharpoonright }_B=G$$
5	1 2 3 4	syl3an	$$⊢\left(F\in \left(C^A\right)\wedge G\in \left(C^B\right)\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to {\left(F\cup G\right)\upharpoonright }_B=G$$