Theorem fin1a2lem1

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

	Ref	Expression
Hypothesis	fin1a2lem.a	$$⊢S=\left(x\in \mathrm{On}⟼\mathrm{suc}x\right)$$
Assertion	fin1a2lem1	$$⊢A\in \mathrm{On}\to S\left(A\right)=\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.a	$$⊢S=\left(x\in \mathrm{On}⟼\mathrm{suc}x\right)$$
2		suceloni	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{On}$$
3		suceq	$$⊢a=A\to \mathrm{suc}a=\mathrm{suc}A$$
4		suceq	$$⊢x=a\to \mathrm{suc}x=\mathrm{suc}a$$
5	4	cbvmptv	$$⊢\left(x\in \mathrm{On}⟼\mathrm{suc}x\right)=\left(a\in \mathrm{On}⟼\mathrm{suc}a\right)$$
6	1 5	eqtri	$$⊢S=\left(a\in \mathrm{On}⟼\mathrm{suc}a\right)$$
7	3 6	fvmptg	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{suc}A\in \mathrm{On}\right)\to S\left(A\right)=\mathrm{suc}A$$
8	2 7	mpdan	$$⊢A\in \mathrm{On}\to S\left(A\right)=\mathrm{suc}A$$