Metamath Proof Explorer


Theorem mapfzcons2

Description: Recover added element 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 M = N + 1
Assertion mapfzcons2 A B 1 N C B A M C M = C

Proof

Step Hyp Ref Expression
1 mapfzcons.1 M = N + 1
2 ovex N + 1 V
3 1 2 eqeltri M V
4 3 a1i A B 1 N C B M V
5 elex C B C V
6 5 adantl A B 1 N C B C V
7 elmapi A B 1 N A : 1 N B
8 7 fdmd A B 1 N dom A = 1 N
9 8 adantr A B 1 N C B dom A = 1 N
10 9 ineq1d A B 1 N C B dom A M = 1 N M
11 1 sneqi M = N + 1
12 11 ineq2i 1 N M = 1 N N + 1
13 fzp1disj 1 N N + 1 =
14 12 13 eqtri 1 N M =
15 10 14 eqtrdi A B 1 N C B dom A M =
16 disjsn dom A M = ¬ M dom A
17 15 16 sylib A B 1 N C B ¬ M dom A
18 fsnunfv M V C V ¬ M dom A A M C M = C
19 4 6 17 18 syl3anc A B 1 N C B A M C M = C