Theorem elmapresaun

Description: fresaun transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

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

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		fresaun	|- ( ( F : A --> C /\ G : B --> C /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) : ( A u. B ) --> C )
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 ) : ( A u. B ) --> C )
6		elmapex	|- ( F e. ( C ^m A ) -> ( C e. _V /\ A e. _V ) )
7	6	simpld	|- ( F e. ( C ^m A ) -> C e. _V )
8	7	3ad2ant1	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> C e. _V )
9	6	simprd	|- ( F e. ( C ^m A ) -> A e. _V )
10		elmapex	|- ( G e. ( C ^m B ) -> ( C e. _V /\ B e. _V ) )
11	10	simprd	|- ( G e. ( C ^m B ) -> B e. _V )
12		unexg	|- ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
13	9 11 12	syl2an	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) ) -> ( A u. B ) e. _V )
14	13	3adant3	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( A u. B ) e. _V )
15	8 14	elmapd	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) e. ( C ^m ( A u. B ) ) <-> ( F u. G ) : ( A u. B ) --> C ) )
16	5 15	mpbird	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) e. ( C ^m ( A u. B ) ) )