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 ... 𝑀 ) ) )