Metamath Proof Explorer

Theorem mapfzcons

Description: Extending a one-based mapping by adding a tuple at the end results in another 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 mapfzcons 
|- ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A u. { <. M , C >. } ) e. ( B ^m ( 1 ... M ) ) )

Proof

Step Hyp Ref Expression
1 mapfzcons.1 
 |-  M = ( N + 1 )
2 simp2 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> A e. ( B ^m ( 1 ... N ) ) )
3 elmapex 
 |-  ( A e. ( B ^m ( 1 ... N ) ) -> ( B e. _V /\ ( 1 ... N ) e. _V ) )
4 3 simpld 
 |-  ( A e. ( B ^m ( 1 ... N ) ) -> B e. _V )
5 4 3ad2ant2 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> B e. _V )
6 ovex 
 |-  ( 1 ... N ) e. _V
7 elmapg 
 |-  ( ( B e. _V /\ ( 1 ... N ) e. _V ) -> ( A e. ( B ^m ( 1 ... N ) ) <-> A : ( 1 ... N ) --> B ) )
8 5 6 7 sylancl 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A e. ( B ^m ( 1 ... N ) ) <-> A : ( 1 ... N ) --> B ) )
9 2 8 mpbid 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> A : ( 1 ... N ) --> B )
10 ovex 
 |-  ( N + 1 ) e. _V
11 simp3 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> C e. B )
12 f1osng 
 |-  ( ( ( N + 1 ) e. _V /\ C e. B ) -> { <. ( N + 1 ) , C >. } : { ( N + 1 ) } -1-1-onto-> { C } )
13 10 11 12 sylancr 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> { <. ( N + 1 ) , C >. } : { ( N + 1 ) } -1-1-onto-> { C } )
14 f1of 
 |-  ( { <. ( N + 1 ) , C >. } : { ( N + 1 ) } -1-1-onto-> { C } -> { <. ( N + 1 ) , C >. } : { ( N + 1 ) } --> { C } )
15 13 14 syl 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> { <. ( N + 1 ) , C >. } : { ( N + 1 ) } --> { C } )
16 snssi 
 |-  ( C e. B -> { C } C_ B )
17 16 3ad2ant3 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> { C } C_ B )
18 15 17 fssd 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> { <. ( N + 1 ) , C >. } : { ( N + 1 ) } --> B )
19 fzp1disj 
 |-  ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/)
20 19 a1i 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/) )
21 fun 
 |-  ( ( ( A : ( 1 ... N ) --> B /\ { <. ( N + 1 ) , C >. } : { ( N + 1 ) } --> B ) /\ ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/) ) -> ( A u. { <. ( N + 1 ) , C >. } ) : ( ( 1 ... N ) u. { ( N + 1 ) } ) --> ( B u. B ) )
22 9 18 20 21 syl21anc 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A u. { <. ( N + 1 ) , C >. } ) : ( ( 1 ... N ) u. { ( N + 1 ) } ) --> ( B u. B ) )
23 1z 
 |-  1 e. ZZ
24 simp1 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> N e. NN0 )
25 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
26 1m1e0 
 |-  ( 1 - 1 ) = 0
27 26 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
28 25 27 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
29 24 28 eleqtrdi 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
30 fzsuc2 
 |-  ( ( 1 e. ZZ /\ N e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
31 23 29 30 sylancr 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
32 31 eqcomd 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( 1 ... N ) u. { ( N + 1 ) } ) = ( 1 ... ( N + 1 ) ) )
33 unidm 
 |-  ( B u. B ) = B
34 33 a1i 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( B u. B ) = B )
35 32 34 feq23d 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( A u. { <. ( N + 1 ) , C >. } ) : ( ( 1 ... N ) u. { ( N + 1 ) } ) --> ( B u. B ) <-> ( A u. { <. ( N + 1 ) , C >. } ) : ( 1 ... ( N + 1 ) ) --> B ) )
36 22 35 mpbid 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A u. { <. ( N + 1 ) , C >. } ) : ( 1 ... ( N + 1 ) ) --> B )
37 ovex 
 |-  ( 1 ... ( N + 1 ) ) e. _V
38 elmapg 
 |-  ( ( B e. _V /\ ( 1 ... ( N + 1 ) ) e. _V ) -> ( ( A u. { <. ( N + 1 ) , C >. } ) e. ( B ^m ( 1 ... ( N + 1 ) ) ) <-> ( A u. { <. ( N + 1 ) , C >. } ) : ( 1 ... ( N + 1 ) ) --> B ) )
39 5 37 38 sylancl 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( A u. { <. ( N + 1 ) , C >. } ) e. ( B ^m ( 1 ... ( N + 1 ) ) ) <-> ( A u. { <. ( N + 1 ) , C >. } ) : ( 1 ... ( N + 1 ) ) --> B ) )
40 36 39 mpbird 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A u. { <. ( N + 1 ) , C >. } ) e. ( B ^m ( 1 ... ( N + 1 ) ) ) )
41 1 opeq1i 
 |-  <. M , C >. = <. ( N + 1 ) , C >.
42 41 sneqi 
 |-  { <. M , C >. } = { <. ( N + 1 ) , C >. }
43 42 uneq2i 
 |-  ( A u. { <. M , C >. } ) = ( A u. { <. ( N + 1 ) , C >. } )
44 1 oveq2i 
 |-  ( 1 ... M ) = ( 1 ... ( N + 1 ) )
45 44 oveq2i 
 |-  ( B ^m ( 1 ... M ) ) = ( B ^m ( 1 ... ( N + 1 ) ) )
46 40 43 45 3eltr4g 
 |-  ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A u. { <. M , C >. } ) e. ( B ^m ( 1 ... M ) ) )