This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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