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

Metamath Proof Explorer

Theorem addpiord

Description: Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion addpiord ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 +N 𝐵 ) = ( 𝐴 +o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 opelxpi ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) )
2 fvres ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) → ( ( +o ↾ ( N × N ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( +o ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
3 df-ov ⊢ ( 𝐴 +N 𝐵 ) = ( +N ‘ ⟨ 𝐴 , 𝐵 ⟩ )
4 df-pli ⊢ +N = ( +o ↾ ( N × N ) )
5 4 fveq1i ⊢ ( +N ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( +o ↾ ( N × N ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
6 3 5 eqtri ⊢ ( 𝐴 +N 𝐵 ) = ( ( +o ↾ ( N × N ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7 df-ov ⊢ ( 𝐴 +o 𝐵 ) = ( +o ‘ ⟨ 𝐴 , 𝐵 ⟩ )
8 2 6 7 3eqtr4g ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) → ( 𝐴 +N 𝐵 ) = ( 𝐴 +o 𝐵 ) )
9 1 8 syl ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 +N 𝐵 ) = ( 𝐴 +o 𝐵 ) )