This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )