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