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 ∈ ω
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 ∈ ω
2 hashp1i.2 ⊢ B = suc ⁡ A
3 hashp1i.3 ⊢ A = M
4 hashp1i.4 ⊢ M + 1 = N
5 df-suc ⊢ suc ⁡ A = A ∪ A
6 2 5 eqtri ⊢ B = A ∪ A
7 6 fveq2i ⊢ B = A ∪ A
8 nnfi ⊢ A ∈ ω → A ∈ Fin
9 1 8 ax-mp ⊢ A ∈ Fin
10 nnord ⊢ A ∈ ω → Ord ⁡ A
11 ordirr ⊢ Ord ⁡ A → ¬ A ∈ A
12 1 10 11 mp2b ⊢ ¬ A ∈ A
13 hashunsng ⊢ A ∈ ω → A ∈ Fin ∧ ¬ A ∈ A → A ∪ A = A + 1
14 1 13 ax-mp ⊢ A ∈ Fin ∧ ¬ A ∈ A → A ∪ A = A + 1
15 9 12 14 mp2an ⊢ A ∪ A = A + 1
16 3 oveq1i ⊢ A + 1 = M + 1
17 16 4 eqtri ⊢ A + 1 = N
18 15 17 eqtri ⊢ A ∪ A = N
19 7 18 eqtri ⊢ B = N