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 ... 𝑁 ) ) = 𝐴 )