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

Proof

Step	Hyp	Ref	Expression
1		mapfzcons.1	⊢ 𝑀 = ( 𝑁 + 1 )
2		ovex	⊢ ( 𝑁 + 1 ) ∈ V
3	1 2	eqeltri	⊢ 𝑀 ∈ V
4	3	a1i	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ∧ 𝐶 ∈ 𝐵 ) → 𝑀 ∈ V )
5		elex	⊢ ( 𝐶 ∈ 𝐵 → 𝐶 ∈ V )
6	5	adantl	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ V )
7		elmapi	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ 𝐵 )
8	7	fdmd	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) → dom 𝐴 = ( 1 ... 𝑁 ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ∧ 𝐶 ∈ 𝐵 ) → dom 𝐴 = ( 1 ... 𝑁 ) )
10	9	ineq1d	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ∧ 𝐶 ∈ 𝐵 ) → ( dom 𝐴 ∩ { 𝑀 } ) = ( ( 1 ... 𝑁 ) ∩ { 𝑀 } ) )
11	1	sneqi	⊢ { 𝑀 } = { ( 𝑁 + 1 ) }
12	11	ineq2i	⊢ ( ( 1 ... 𝑁 ) ∩ { 𝑀 } ) = ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } )
13		fzp1disj	⊢ ( ( 1 ... 𝑁 ) ∩ { ( 𝑁 + 1 ) } ) = ∅
14	12 13	eqtri	⊢ ( ( 1 ... 𝑁 ) ∩ { 𝑀 } ) = ∅
15	10 14	eqtrdi	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ∧ 𝐶 ∈ 𝐵 ) → ( dom 𝐴 ∩ { 𝑀 } ) = ∅ )
16		disjsn	⊢ ( ( dom 𝐴 ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀 ∈ dom 𝐴 )
17	15 16	sylib	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ∧ 𝐶 ∈ 𝐵 ) → ¬ 𝑀 ∈ dom 𝐴 )
18		fsnunfv	⊢ ( ( 𝑀 ∈ V ∧ 𝐶 ∈ V ∧ ¬ 𝑀 ∈ dom 𝐴 ) → ( ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) ‘ 𝑀 ) = 𝐶 )
19	4 6 17 18	syl3anc	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐴 ∪ { ⟨ 𝑀 , 𝐶 ⟩ } ) ‘ 𝑀 ) = 𝐶 )