Theorem hashp1i

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

	Ref	Expression
Hypotheses	hashp1i.1	|- A e. _om
	hashp1i.2	|- B = suc A
	hashp1i.3	|- ( # ` A ) = M
	hashp1i.4	|- ( M + 1 ) = N
Assertion	hashp1i	|- ( # ` B ) = N

Proof

Step	Hyp	Ref	Expression
1		hashp1i.1	|- A e. _om
2		hashp1i.2	|- B = suc A
3		hashp1i.3	|- ( # ` A ) = M
4		hashp1i.4	|- ( M + 1 ) = N
5		df-suc	|- suc A = ( A u. { A } )
6	2 5	eqtri	|- B = ( A u. { A } )
7	6	fveq2i	|- ( # ` B ) = ( # ` ( A u. { A } ) )
8		nnfi	|- ( A e. _om -> A e. Fin )
9	1 8	ax-mp	|- A e. Fin
10		nnord	|- ( A e. _om -> Ord A )
11		ordirr	|- ( Ord A -> -. A e. A )
12	1 10 11	mp2b	|- -. A e. A
13		hashunsng	|- ( A e. _om -> ( ( A e. Fin /\ -. A e. A ) -> ( # ` ( A u. { A } ) ) = ( ( # ` A ) + 1 ) ) )
14	1 13	ax-mp	|- ( ( A e. Fin /\ -. A e. A ) -> ( # ` ( A u. { A } ) ) = ( ( # ` A ) + 1 ) )
15	9 12 14	mp2an	|- ( # ` ( A u. { A } ) ) = ( ( # ` A ) + 1 )
16	3	oveq1i	|- ( ( # ` A ) + 1 ) = ( M + 1 )
17	16 4	eqtri	|- ( ( # ` A ) + 1 ) = N
18	15 17	eqtri	|- ( # ` ( A u. { A } ) ) = N
19	7 18	eqtri	|- ( # ` B ) = N