Metamath Proof Explorer

Theorem mapfzcons1

Description: Recover prefix mapping 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 mapfzcons1 
|- ( A e. ( B ^m ( 1 ... N ) ) -> ( ( A u. { <. M , C >. } ) |` ( 1 ... N ) ) = A )

Proof

Step Hyp Ref Expression
1 mapfzcons.1 
 |-  M = ( N + 1 )
2 elmapi 
 |-  ( A e. ( B ^m ( 1 ... N ) ) -> A : ( 1 ... N ) --> B )
3 ffn 
 |-  ( A : ( 1 ... N ) --> B -> A Fn ( 1 ... N ) )
4 fnresdm 
 |-  ( A Fn ( 1 ... N ) -> ( A |` ( 1 ... N ) ) = A )
5 2 3 4 3syl 
 |-  ( A e. ( B ^m ( 1 ... N ) ) -> ( A |` ( 1 ... N ) ) = A )
6 5 uneq1d 
 |-  ( A e. ( B ^m ( 1 ... N ) ) -> ( ( A |` ( 1 ... N ) ) u. ( { <. M , C >. } |` ( 1 ... N ) ) ) = ( A u. ( { <. M , C >. } |` ( 1 ... N ) ) ) )
7 resundir 
 |-  ( ( A u. { <. M , C >. } ) |` ( 1 ... N ) ) = ( ( A |` ( 1 ... N ) ) u. ( { <. M , C >. } |` ( 1 ... N ) ) )
8 dmres 
 |-  dom ( { <. M , C >. } |` ( 1 ... N ) ) = ( ( 1 ... N ) i^i dom { <. M , C >. } )
9 dmsnopss 
 |-  dom { <. M , C >. } C_ { M }
10 1 sneqi 
 |-  { M } = { ( N + 1 ) }
11 9 10 sseqtri 
 |-  dom { <. M , C >. } C_ { ( N + 1 ) }
12 sslin 
 |-  ( dom { <. M , C >. } C_ { ( N + 1 ) } -> ( ( 1 ... N ) i^i dom { <. M , C >. } ) C_ ( ( 1 ... N ) i^i { ( N + 1 ) } ) )
13 11 12 ax-mp 
 |-  ( ( 1 ... N ) i^i dom { <. M , C >. } ) C_ ( ( 1 ... N ) i^i { ( N + 1 ) } )
14 fzp1disj 
 |-  ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/)
15 sseq0 
 |-  ( ( ( ( 1 ... N ) i^i dom { <. M , C >. } ) C_ ( ( 1 ... N ) i^i { ( N + 1 ) } ) /\ ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/) ) -> ( ( 1 ... N ) i^i dom { <. M , C >. } ) = (/) )
16 13 14 15 mp2an 
 |-  ( ( 1 ... N ) i^i dom { <. M , C >. } ) = (/)
17 8 16 eqtri 
 |-  dom ( { <. M , C >. } |` ( 1 ... N ) ) = (/)
18 relres 
 |-  Rel ( { <. M , C >. } |` ( 1 ... N ) )
19 reldm0 
 |-  ( Rel ( { <. M , C >. } |` ( 1 ... N ) ) -> ( ( { <. M , C >. } |` ( 1 ... N ) ) = (/) <-> dom ( { <. M , C >. } |` ( 1 ... N ) ) = (/) ) )
20 18 19 ax-mp 
 |-  ( ( { <. M , C >. } |` ( 1 ... N ) ) = (/) <-> dom ( { <. M , C >. } |` ( 1 ... N ) ) = (/) )
21 17 20 mpbir 
 |-  ( { <. M , C >. } |` ( 1 ... N ) ) = (/)
22 21 uneq2i 
 |-  ( A u. ( { <. M , C >. } |` ( 1 ... N ) ) ) = ( A u. (/) )
23 un0 
 |-  ( A u. (/) ) = A
24 22 23 eqtr2i 
 |-  A = ( A u. ( { <. M , C >. } |` ( 1 ... N ) ) )
25 6 7 24 3eqtr4g 
 |-  ( A e. ( B ^m ( 1 ... N ) ) -> ( ( A u. { <. M , C >. } ) |` ( 1 ... N ) ) = A )