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 ⊢ 𝑀 = ( 𝑁 + 1 )
Assertion mapfzcons1 ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) → ( ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 mapfzcons.1 ⊢ 𝑀 = ( 𝑁 + 1 )
2 elmapi ⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ 𝐵 )
3 ffn ⊢ ( 𝐴 : ( 1 ... 𝑁 ) ⟶ 𝐵 → 𝐴 Fn ( 1 ... 𝑁 ) )
4 fnresdm ⊢ ( 𝐴 Fn ( 1 ... 𝑁 ) → ( 𝐴 ↾ ( 1 ... 𝑁 ) ) = 𝐴 )
5 2 3 4 3syl ⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) → ( 𝐴 ↾ ( 1 ... 𝑁 ) ) = 𝐴 )
6 5 uneq1d ⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) → ( ( 𝐴 ↾ ( 1 ... 𝑁 ) ) ∪ ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) ) = ( 𝐴 ∪ ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) ) )
7 resundir ⊢ ( ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) = ( ( 𝐴 ↾ ( 1 ... 𝑁 ) ) ∪ ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) )
8 dmres ⊢ dom ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∩ dom { ⟨ 𝑀 , 𝐶 ⟩ } )
9 dmsnopss ⊢ dom { ⟨ 𝑀 , 𝐶 ⟩ } ⊆ { 𝑀 }
10 1 sneqi ⊢ { 𝑀 } = { ( 𝑁 + 1 ) }
11 9 10 sseqtri ⊢ dom { ⟨ 𝑀 , 𝐶 ⟩ } ⊆ { ( 𝑁 + 1 ) }
12 sslin ⊢ ( dom { ⟨ 𝑀 , 𝐶 ⟩ } ⊆ { ( 𝑁 + 1 ) } → ( ( 1 ... 𝑁 ) ∩ dom { ⟨ 𝑀 , 𝐶 ⟩ } ) ⊆ ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) )
13 11 12 ax-mp ⊢ ( ( 1 ... 𝑁 ) ∩ dom { ⟨ 𝑀 , 𝐶 ⟩ } ) ⊆ ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } )
14 fzp1disj ⊢ ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅
15 sseq0 ⊢ ( ( ( ( 1 ... 𝑁 ) ∩ dom { ⟨ 𝑀 , 𝐶 ⟩ } ) ⊆ ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) ∧ ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅ ) → ( ( 1 ... 𝑁 ) ∩ dom { ⟨ 𝑀 , 𝐶 ⟩ } ) = ∅ )
16 13 14 15 mp2an ⊢ ( ( 1 ... 𝑁 ) ∩ dom { ⟨ 𝑀 , 𝐶 ⟩ } ) = ∅
17 8 16 eqtri ⊢ dom ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) = ∅
18 relres ⊢ Rel ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) )
19 reldm0 ⊢ ( Rel ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) → ( ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) = ∅ ↔ dom ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) = ∅ ) )
20 18 19 ax-mp ⊢ ( ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) = ∅ ↔ dom ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) = ∅ )
21 17 20 mpbir ⊢ ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) = ∅
22 21 uneq2i ⊢ ( 𝐴 ∪ ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) ) = ( 𝐴 ∪ ∅ )
23 un0 ⊢ ( 𝐴 ∪ ∅ ) = 𝐴
24 22 23 eqtr2i ⊢ 𝐴 = ( 𝐴 ∪ ( { ⟨ 𝑀 , 𝐶 ⟩ } ↾ ( 1 ... 𝑁 ) ) )
25 6 7 24 3eqtr4g ⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) → ( ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) ↾ ( 1 ... 𝑁 ) ) = 𝐴 )