Theorem mapco2g

Description: Renaming indices in a tuple, with sethood as antecedents. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	mapco2g	|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) e. ( B ^m E ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	|- ( A e. ( B ^m C ) -> A : C --> B )
2		fco	|- ( ( A : C --> B /\ D : E --> C ) -> ( A o. D ) : E --> B )
3	1 2	sylan	|- ( ( A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) : E --> B )
4	3	3adant1	|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) : E --> B )
5		n0i	|- ( A e. ( B ^m C ) -> -. ( B ^m C ) = (/) )
6		reldmmap	|- Rel dom ^m
7	6	ovprc1	|- ( -. B e. _V -> ( B ^m C ) = (/) )
8	5 7	nsyl2	|- ( A e. ( B ^m C ) -> B e. _V )
9	8	3ad2ant2	|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> B e. _V )
10		simp1	|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> E e. _V )
11	9 10	elmapd	|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> ( ( A o. D ) e. ( B ^m E ) <-> ( A o. D ) : E --> B ) )
12	4 11	mpbird	|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) e. ( B ^m E ) )