Theorem mapfzcons2

Description: Recover added element from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014) (Revised by Stefan O'Rear, 5-May-2015)

	Ref	Expression
Hypothesis	mapfzcons.1	|- M = ( N + 1 )
Assertion	mapfzcons2	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( A u. { <. M , C >. } ) ` M ) = C )

Proof

Step	Hyp	Ref	Expression
1		mapfzcons.1	|- M = ( N + 1 )
2		ovex	|- ( N + 1 ) e. _V
3	1 2	eqeltri	|- M e. _V
4	3	a1i	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> M e. _V )
5		elex	|- ( C e. B -> C e. _V )
6	5	adantl	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> C e. _V )
7		elmapi	|- ( A e. ( B ^m ( 1 ... N ) ) -> A : ( 1 ... N ) --> B )
8	7	fdmd	|- ( A e. ( B ^m ( 1 ... N ) ) -> dom A = ( 1 ... N ) )
9	8	adantr	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> dom A = ( 1 ... N ) )
10	9	ineq1d	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( dom A i^i { M } ) = ( ( 1 ... N ) i^i { M } ) )
11	1	sneqi	|- { M } = { ( N + 1 ) }
12	11	ineq2i	|- ( ( 1 ... N ) i^i { M } ) = ( ( 1 ... N ) i^i { ( N + 1 ) } )
13		fzp1disj	|- ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/)
14	12 13	eqtri	|- ( ( 1 ... N ) i^i { M } ) = (/)
15	10 14	eqtrdi	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( dom A i^i { M } ) = (/) )
16		disjsn	|- ( ( dom A i^i { M } ) = (/) <-> -. M e. dom A )
17	15 16	sylib	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> -. M e. dom A )
18		fsnunfv	|- ( ( M e. _V /\ C e. _V /\ -. M e. dom A ) -> ( ( A u. { <. M , C >. } ) ` M ) = C )
19	4 6 17 18	syl3anc	|- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( A u. { <. M , C >. } ) ` M ) = C )