Theorem hashp1i

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

	Ref	Expression
Hypotheses	hashp1i.1	⊢ 𝐴 ∈ ω
	hashp1i.2	⊢ 𝐵 = suc 𝐴
	hashp1i.3	⊢ ( ♯ ‘ 𝐴 ) = 𝑀
	hashp1i.4	⊢ ( 𝑀 + 1 ) = 𝑁
Assertion	hashp1i	⊢ ( ♯ ‘ 𝐵 ) = 𝑁

Proof

Step	Hyp	Ref	Expression
1		hashp1i.1	⊢ 𝐴 ∈ ω
2		hashp1i.2	⊢ 𝐵 = suc 𝐴
3		hashp1i.3	⊢ ( ♯ ‘ 𝐴 ) = 𝑀
4		hashp1i.4	⊢ ( 𝑀 + 1 ) = 𝑁
5		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
6	2 5	eqtri	⊢ 𝐵 = ( 𝐴 ∪ { 𝐴 } )
7	6	fveq2i	⊢ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( 𝐴 ∪ { 𝐴 } ) )
8		nnfi	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
9	1 8	ax-mp	⊢ 𝐴 ∈ Fin
10		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
11		ordirr	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
12	1 10 11	mp2b	⊢ ¬ 𝐴 ∈ 𝐴
13		hashunsng	⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ∈ Fin ∧ ¬ 𝐴 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐴 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
14	1 13	ax-mp	⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐴 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐴 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
15	9 12 14	mp2an	⊢ ( ♯ ‘ ( 𝐴 ∪ { 𝐴 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 )
16	3	oveq1i	⊢ ( ( ♯ ‘ 𝐴 ) + 1 ) = ( 𝑀 + 1 )
17	16 4	eqtri	⊢ ( ( ♯ ‘ 𝐴 ) + 1 ) = 𝑁
18	15 17	eqtri	⊢ ( ♯ ‘ ( 𝐴 ∪ { 𝐴 } ) ) = 𝑁
19	7 18	eqtri	⊢ ( ♯ ‘ 𝐵 ) = 𝑁