Theorem fin1a2lem1

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypothesis	fin1a2lem.a	⊢ 𝑆 = ( 𝑥 ∈ On ↦ suc 𝑥 )
Assertion	fin1a2lem1	⊢ ( 𝐴 ∈ On → ( 𝑆 ‘ 𝐴 ) = suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.a	⊢ 𝑆 = ( 𝑥 ∈ On ↦ suc 𝑥 )
2		suceloni	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
3		suceq	⊢ ( 𝑎 = 𝐴 → suc 𝑎 = suc 𝐴 )
4		suceq	⊢ ( 𝑥 = 𝑎 → suc 𝑥 = suc 𝑎 )
5	4	cbvmptv	⊢ ( 𝑥 ∈ On ↦ suc 𝑥 ) = ( 𝑎 ∈ On ↦ suc 𝑎 )
6	1 5	eqtri	⊢ 𝑆 = ( 𝑎 ∈ On ↦ suc 𝑎 )
7	3 6	fvmptg	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ On ) → ( 𝑆 ‘ 𝐴 ) = suc 𝐴 )
8	2 7	mpdan	⊢ ( 𝐴 ∈ On → ( 𝑆 ‘ 𝐴 ) = suc 𝐴 )