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 𝑀 = ( 𝑁 + 1 )
Assertion mapfzcons ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) ∈ ( 𝐵m ( 1 ... 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 mapfzcons.1 𝑀 = ( 𝑁 + 1 )
2 simp2 ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → 𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) )
3 elmapex ( 𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) → ( 𝐵 ∈ V ∧ ( 1 ... 𝑁 ) ∈ V ) )
4 3 simpld ( 𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) → 𝐵 ∈ V )
5 4 3ad2ant2 ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → 𝐵 ∈ V )
6 ovex ( 1 ... 𝑁 ) ∈ V
7 elmapg ( ( 𝐵 ∈ V ∧ ( 1 ... 𝑁 ) ∈ V ) → ( 𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ 𝐵 ) )
8 5 6 7 sylancl ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ 𝐵 ) )
9 2 8 mpbid ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ 𝐵 )
10 ovex ( 𝑁 + 1 ) ∈ V
11 simp3 ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → 𝐶𝐵 )
12 f1osng ( ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶𝐵 ) → { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } –1-1-onto→ { 𝐶 } )
13 10 11 12 sylancr ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } –1-1-onto→ { 𝐶 } )
14 f1of ( { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } –1-1-onto→ { 𝐶 } → { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } ⟶ { 𝐶 } )
15 13 14 syl ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } ⟶ { 𝐶 } )
16 snssi ( 𝐶𝐵 → { 𝐶 } ⊆ 𝐵 )
17 16 3ad2ant3 ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → { 𝐶 } ⊆ 𝐵 )
18 15 17 fssd ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } ⟶ 𝐵 )
19 fzp1disj ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅
20 19 a1i ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ )
21 fun ( ( ( 𝐴 : ( 1 ... 𝑁 ) ⟶ 𝐵 ∧ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } : { ( 𝑁 + 1 ) } ⟶ 𝐵 ) ∧ ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ ) → ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( ( 1 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ⟶ ( 𝐵𝐵 ) )
22 9 18 20 21 syl21anc ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( ( 1 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ⟶ ( 𝐵𝐵 ) )
23 1z 1 ∈ ℤ
24 simp1 ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → 𝑁 ∈ ℕ0 )
25 nn0uz 0 = ( ℤ ‘ 0 )
26 1m1e0 ( 1 − 1 ) = 0
27 26 fveq2i ( ℤ ‘ ( 1 − 1 ) ) = ( ℤ ‘ 0 )
28 25 27 eqtr4i 0 = ( ℤ ‘ ( 1 − 1 ) )
29 24 28 eleqtrdi ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → 𝑁 ∈ ( ℤ ‘ ( 1 − 1 ) ) )
30 fzsuc2 ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ ( 1 − 1 ) ) ) → ( 1 ... ( 𝑁 + 1 ) ) = ( ( 1 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
31 23 29 30 sylancr ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 1 ... ( 𝑁 + 1 ) ) = ( ( 1 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) )
32 31 eqcomd ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( ( 1 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) = ( 1 ... ( 𝑁 + 1 ) ) )
33 unidm ( 𝐵𝐵 ) = 𝐵
34 33 a1i ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 𝐵𝐵 ) = 𝐵 )
35 32 34 feq23d ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( ( 1 ... 𝑁 ) ∪ { ( 𝑁 + 1 ) } ) ⟶ ( 𝐵𝐵 ) ↔ ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ 𝐵 ) )
36 22 35 mpbid ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ 𝐵 )
37 ovex ( 1 ... ( 𝑁 + 1 ) ) ∈ V
38 elmapg ( ( 𝐵 ∈ V ∧ ( 1 ... ( 𝑁 + 1 ) ) ∈ V ) → ( ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ∈ ( 𝐵m ( 1 ... ( 𝑁 + 1 ) ) ) ↔ ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ 𝐵 ) )
39 5 37 38 sylancl ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ∈ ( 𝐵m ( 1 ... ( 𝑁 + 1 ) ) ) ↔ ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) : ( 1 ... ( 𝑁 + 1 ) ) ⟶ 𝐵 ) )
40 36 39 mpbird ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ∈ ( 𝐵m ( 1 ... ( 𝑁 + 1 ) ) ) )
41 1 opeq1i 𝑀 , 𝐶 ⟩ = ⟨ ( 𝑁 + 1 ) , 𝐶
42 41 sneqi { ⟨ 𝑀 , 𝐶 ⟩ } = { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ }
43 42 uneq2i ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) = ( 𝐴 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
44 1 oveq2i ( 1 ... 𝑀 ) = ( 1 ... ( 𝑁 + 1 ) )
45 44 oveq2i ( 𝐵m ( 1 ... 𝑀 ) ) = ( 𝐵m ( 1 ... ( 𝑁 + 1 ) ) )
46 40 43 45 3eltr4g ( ( 𝑁 ∈ ℕ0𝐴 ∈ ( 𝐵m ( 1 ... 𝑁 ) ) ∧ 𝐶𝐵 ) → ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) ∈ ( 𝐵m ( 1 ... 𝑀 ) ) )