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 ⊢ 𝐴 ∈ ω
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 ⊢ ( ♯ ‘ 𝐵 ) = 𝑁