Theorem hashp1i

Description: Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Hypotheses	hashp1i.1	$$⊢A\in \mathrm{\omega }$$
	hashp1i.2	$$⊢B=\mathrm{suc}A$$
	hashp1i.3	$$⊢\left|A\right|=M$$
	hashp1i.4	$$⊢M+1=N$$
Assertion	hashp1i	$$⊢\left|B\right|=N$$

Proof

Step	Hyp	Ref	Expression
1		hashp1i.1	$$⊢A\in \mathrm{\omega }$$
2		hashp1i.2	$$⊢B=\mathrm{suc}A$$
3		hashp1i.3	$$⊢\left|A\right|=M$$
4		hashp1i.4	$$⊢M+1=N$$
5		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
6	2 5	eqtri	$$⊢B=A\cup \left\{A\right\}$$
7	6	fveq2i	$$⊢\left|B\right|=\left|A\cup \left\{A\right\}\right|$$
8		nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$
9	1 8	ax-mp	$$⊢A\in \mathrm{Fin}$$
10		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
11		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
12	1 10 11	mp2b	$$⊢\neg A\in A$$
13		hashunsng	$$⊢A\in \mathrm{\omega }\to \left(\left(A\in \mathrm{Fin}\wedge \neg A\in A\right)\to \left|A\cup \left\{A\right\}\right|=\left|A\right|+1\right)$$
14	1 13	ax-mp	$$⊢\left(A\in \mathrm{Fin}\wedge \neg A\in A\right)\to \left|A\cup \left\{A\right\}\right|=\left|A\right|+1$$
15	9 12 14	mp2an	$$⊢\left|A\cup \left\{A\right\}\right|=\left|A\right|+1$$
16	3	oveq1i	$$⊢\left|A\right|+1=M+1$$
17	16 4	eqtri	$$⊢\left|A\right|+1=N$$
18	15 17	eqtri	$$⊢\left|A\cup \left\{A\right\}\right|=N$$
19	7 18	eqtri	$$⊢\left|B\right|=N$$