Theorem elmapresaunres2

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

	Ref	Expression
Assertion	elmapresaunres2	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = G )

Proof

Step	Hyp	Ref	Expression
1		elmapi	|- ( F e. ( C ^m A ) -> F : A --> C )
2		elmapi	|- ( G e. ( C ^m B ) -> G : B --> C )
3		id	|- ( ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) -> ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) )
4		fresaunres2	|- ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = G )
5	1 2 3 4	syl3an	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = G )